package coq-corn

CoRN includes the following parts:

• Algebraic Hierarchy

  An axiomatic formalization of the most common algebraic structures, including setoids, monoids, groups, rings, fields, ordered fields, rings of polynomials, real and complex numbers

• Model of the Real Numbers

  Construction of a concrete real number structure satisfying the previously defined axioms

• Fundamental Theorem of Algebra

  A proof that every non-constant polynomial on the complex plane has at least one root

• Real Calculus

  A collection of elementary results on real analysis, including continuity, differentiability, integration, Taylor's theorem and the Fundamental Theorem of Calculus

• Exact Real Computation

  Fast verified computation inside Coq. This includes: real numbers, functions, integrals, graphs of functions, differential equations.