CoqInterval
Tactics for performing proofs of inequalities on expressions of real numbers.
- from
- Coq
- added
- 2026-10-10
- likes
- 0
similar
-
Coq Exchange: ideas and experiment reports about Coq project.inria.fr
-
Coquelicot gitlab.inria.fr
Formalization of classical real analysis compatible with the standard library and focusing on usability.
-
Proofs and Reliable Programming using Coq team.inria.fr
Introduction to developing and verifying programs with Coq.
-
MathComp School github.com
Coq sources for lessons and exercises that introduce the SSReflect proof language and the Mathematical Components library.
-
Programs and Proofs ilyasergey.net
Book that gives a brief and practically-oriented introduction to interactive proofs in Coq which emphasizes the computational nature of inductive reasoning about decidable propositions via a small set of primitives from the SSReflect proof language.
-
Official Coq standard library coq.inria.fr
Coq › Projects > Libraries: “Tactics for performing proofs of inequalities on expressions of real numbers.”