Formalizing 100 theorems in Coq

many versions(e.g. one in contribs/QArithSternBrocot/sqrt2 ):

Theorem sqrt2_not_rational : forall p q, q <> 0 -> p * p <> q * q * 2.

Herman Geuvers et al.(in C-CoRN/fta/FTA ):

Lemma FTA : forall f : CCX, nonConst _ f -> {z : CC | f ! z [=] [0]}.

Milad Niqui(in contribs/QArithSternBrocot/Q_denumerable ):

Theorem Q_is_denumerable: same_cardinality Q nat.

Definition same_cardinality (A:Set) (B:Set) :=
  { f : A -> B &
  { g : B -> A |
    forall b,(compose _ _ _ f g) b = (identity B) b /\
    forall a,(compose _ _ _ g f) a = (identity A) a
  }}.

Inductive CountableT (X:Type) : Prop :=
  | intro_nat_injection: forall f:X->nat, injective f -> CountableT X.

Lemma Q_countable: CountableT Q.

Frédérique Guilhot( contribs/HighSchoolGeometry/euclidien_classiques ):

Theorem Pythagore :
 forall A B C : PO,
 orthogonal (vec A B) (vec A C) <->
 Rsqr (distance B C) = Rsqr (distance A B) + Rsqr (distance A C) :>R.

Gabriel Braun (GeoCoq in Chapter 15 ) :

A synthetic proof in the context of Tarski's axioms.

Lemma pythagoras :
 forall O E E' A B C AC BC AB AC2 BC2 AB2,
  O<>E ->
  Per A C B ->
  length O E E' A B AB ->
  length O E E' A C AC ->
  length O E E' B C BC ->
  prod O E E' AC AC AC2 ->
  prod O E E' BC BC BC2 ->
  prod O E E' AB AB AB2 ->
  sum  O E E' AC2 BC2 AB2.

Russell O'Connor( in contribs/Goedel/goedel1 , see description on r6.ca and proof archive: Goedel20050512.tar.gz ):

Theorem Goedel'sIncompleteness1st :
 wConsistent T ->
 exists f : Formula,
   ~ SysPrf T f /\
   ~ SysPrf T (notH f) /\ (forall v : nat, ~ In v (freeVarFormula LNN f)).

Russell O'Connor proved the theorem under the assumption of the last two Hilbert-Bernays-Loeb derivability conditions.

Hypothesis HBL2 : forall f, SysPrf T (impH (box f) (box (box f))).
Hypothesis HBL3 : forall f g, SysPrf T (impH (box (impH f g)) (impH (box f) (box g))).

Theorem SecondIncompletness :
SysPrf T Con -> Inconsistent LNT T.

Nathanaël Courant( proof on github ):

Theorem Quadratic_reciprocity :
  (legendre p q) * (legendre q p) = (-1) ^ (((p - 1) / 2) * ((q - 1) / 2)).

Laurent Théry(in mathcomp/solvable/cyclic.v ):

Theorem Euler_exp_totient a n : coprime a n -> a ^ totient n  = 1 %[mod n].

Russell O'Connor( in cocorico , compatible with coq 7.3):

Theorem ManyPrimes : ~(EX l:(list Prime) | (p:Prime)(In p l)).

Jean-François Dufourd(in contribs/EulerFormula/Euler3 ):

nc : number of connected components
nv : number of vertices
ne : number of edges
nf : number of faces
nd : number of darts
plf m : m is a planar formation
inv_qhmap : see Euler1.v

Theorem Euler_Poincare_criterion: forall m:fmap,
  inv_qhmap m -> (plf m <-> (nv m + ne m + nf m - nd m) / 2 = nc m).

Jean-Marie Madiot( in Coqtail/Reals/Rzeta2 ):

Theorem zeta2_pi_2_6 : Rser_cv (fun n => 1 / (n + 1) ^ 2) (PI ^ 2 / 6).

Luís Cruz-Filipe(in C-CoRN/ftc/FTC ):

Theorem FTC1 : Derivative J pJ G F.
Theorem FTC2 : {c : IR | Feq J (G{-}G0) [-C-]c}.

Lemma FTC_Riemann :
  forall (f:C1_fun) (a b:R) (pr:Riemann_integrable (derive f (diff0 f)) a b),
    RiemannInt pr = f b - f a.

Coqtail team( in Coqtail/Complex/Cexp ):

De Moivre's formula is easily deduced from Euler's formula thanks to e^(n*z)=(e^z)^n.

Lemma Cexp_trigo_compat : forall a, Cexp (0 +i a) = cos a +i sin a.
Lemma Cexp_mult : forall a n, Cexp (INC n * a) = (Cexp a) ^ n.

Valentin Blot(see Valentin's website or directly the .tar.gz of the proof ):

Theorem Liouville_theorem2 :
    {n : nat | {C : IR | Zero [<] C | forall (x : Q),
         (C[*]inj_Q IR (1#Qden x)%Q[^]n) [<=] AbsIR (inj_Q _ x [-] a)}}.

Guillaume Allais, Jean-Marie Madiot(in Coqtail/Arith/Lagrange_four_square ):

"{a | P}" means "there exists a such that P" but in a constructive setting. Indeed, from the proof, we can extract a program computing a, b, c, d from n.

Theorem lagrange_4_square_theorem : forall n, 0 <= n ->
  { a : _ & { b: _ & { c : _ & { d |
    n = a * a + b * b + c * c + d * d } } } }.

Laurent Théry(in contribs/SumOfTwoSquare/TwoSquares ):

Definition sum_of_two_squares :=
   fun p => exists a , exists b , p = a * a + b * b.

Theorem two_squares_sum:
 forall n,
 0 <= n ->
 (forall p, prime p -> Zis_mod p 3 4 ->  Zeven (Zdiv_exp p n)) ->
  sum_of_two_squares n.

Pierre-Marie Pédrot(in Coqtail/Reals/Logic/Runcountable ):

Theorem R_uncountable : forall (f : nat -> R),
  {l : R | forall n, l <> f n}.

Theorem R_uncountable_strong : forall (f : nat -> R) (x y : R),
  x < y -> {l : R | forall n, l <> f n & x <= l <= y}.

Theorem reals_not_countable :
  forall (f : nat -> IR), {x :IR | forall n : nat, x [#] (f n)}.

David Delahaye(in contribs/Fermat4/Pythagorean ):

Lemma pytha_thm3 : forall a b c : Z,
  is_pytha a b c -> Zodd a ->
  exists p : Z, exists q : Z, exists m : Z,
    a = m * (q * q - p * p) /\ b = 2 * m * (p * q) /\
    c = m * (p * p + q * q) /\ m >= 0 /\
    p >= 0 /\ q > 0 /\ p <= q /\ (rel_prime p q) /\
    (distinct_parity p q).

Hugo Herbelin(in contribs/Schroeder/Schroeder ):

Theorem Schroeder : A <=_card B -> B <=_card A -> A =_card B.

Section CSB.
Variable X Y:Type.
Variable f:X->Y.
Variable g:Y->X.
Hypothesis f_inj: injective f.
Hypothesis g_inj: injective g.

Theorem CSB: exists h:X->Y, bijective h.

End CSB.

Guillaume Allais(in standard library, Reals/Ratan ):

Lemma PI_2_aux : {z : R | 7 / 8 <= z <= 7 / 4 /\ - cos z = 0}.
Definition PI := 2 * proj1_sig PI_2_aux.

Definition PI_tg n := / INR (2 * n + 1).
Lemma exists_PI : {l:R | Un_cv (fun N => sum_f_R0 (tg_alt PI_tg) N) l}.
Definition Alt_PI : R := 4 * (let (a,_) := exist_PI in a).

Theorem Alt_PI_eq : Alt_PI = PI.

Lemma ArcTan_one : ArcTan One[=]Pi[/]FourNZ.

Lemma arctan_series : forall c : IR,
  forall (Hs :
    fun_series_convergent_IR
      (olor ([--]One) One)
      (fun i =>
        (([--]One)[^]i[/]nring (S (2*i))
        [//] nringS_ap_zero _ (2*i)){**}Fid IR{^}(2*i+1)))
    Hc,
       FSeries_Sum Hs c Hc[=]ArcTan c.

Frédérique Guilhot(in contribs/HighSchoolGeometry/angles_vecteurs ):

Theorem somme_triangle :
 forall A B C : PO,
 A <> B :>PO ->
 A <> C :>PO ->
 B <> C :>PO ->
 plus (cons_AV (vec A B) (vec A C))
   (plus (cons_AV (vec B C) (vec B A)) (cons_AV (vec C A) (vec C B))) =
 image_angle pi :>AV.

Boutry, Gries, Narboux(in GeoCoq/Meta_theory/Parallel_postulates/Euclid ):

It is shown that the sum of angles is two rights is equivalent to other versions of the parallel postulate.

Theorem equivalent_parallel_postulates_assuming_greenberg_s_postulate :
  greenberg_s_postulate ->
  all_equiv
    (alternate_interior_angles_postulate::
     alternative_playfair_s_postulate::
     alternative_proclus_postulate::
     alternative_strong_parallel_postulate::
     consecutive_interior_angles_postulate::
     euclid_5::
     euclid_s_parallel_postulate::
     existential_playfair_s_postulate::
     existential_thales_postulate::
     inverse_projection_postulate::
     midpoint_converse_postulate::
     perpendicular_transversal_postulate::
     playfair_s_postulate::
     posidonius_postulate::
     posidonius_second_postulate::
     postulate_of_existence_of_a_right_lambert_quadrilateral::
     postulate_of_existence_of_a_right_saccheri_quadrilateral::
     postulate_of_existence_of_a_triangle_whose_angles_sum_to_2_rights::
     postulate_of_existence_of_similar_triangles::
     postulate_of_parallelism_of_perpendicular_transversals::
     postulate_of_right_lambert_quadrilaterals::
     postulate_of_right_saccheri_quadrilaterals::
     postulate_of_transitivity_of_parallelism::
     proclus_postulate::
     strong_parallel_postulate::
     tarski_s_parallel_postulate::
     thales_postulate::
     thales_converse_postulate::
     triangle_circumscription_principle::
     triangle_postulate::
     nil).

Magaud and Narboux(in contribs/ProjectiveGeometry/plane/hexamys ):

Definition is_hexamy A B C D E F :=
  (A<>B / A<>C / A<>D / A<>E / A<>F /
  B<>C / B<>D / B<>E / B<>F /
  C<>D / C<>E / C<>F /
  D<>E / D<>F /
  E<>F) /
  let a:= inter (line B C) (line E F) in
  let b:= inter (line C D) (line F A) in
  let c:= inter (line A B) (line D E) in
Col a b c.

Lemma hexamy_prop: pappus_strong -> forall A B C D E F,
 (line C D) <> (line A F) ->
 (line B C) <> (line E F) ->
 (line A B) <> (line D E) ->

 (line A C) <> (line E F) ->
 (line B F) <> (line C D) ->
 is_hexamy A B C D E F -> is_hexamy B A C D E F.

CertiGeo team, marelle project(in CertiGeo/feuerbach ):

Lemma Feuerbach:  forall A B C A1 B1 C1 O A2 B2 C2 O2:point,
  forall r r2:R,
  X A = 0 -> Y A =  0 -> X B = 1 -> Y B =  0->
  middle A B C1 -> middle B C A1 -> middle C A B1 ->
  distance2 O A1 = distance2 O B1 ->
  distance2 O A1 = distance2 O C1 ->
  collinear A B C2 -> orthogonal A B O2 C2 ->
  collinear B C A2 -> orthogonal B C O2 A2 ->
  collinear A C B2 -> orthogonal A C O2 B2 ->
  distance2 O2 A2 = distance2 O2 B2 ->
  distance2 O2 A2 = distance2 O2 C2 ->
  r^2 = distance2 O A1 ->
  r2^2 = distance2 O2 A2 ->
  distance2 O O2 = (r + r2)^2
  \/ distance2 O O2 = (r - r2)^2
  \/ collinear A B C.

Jean-Marie Madiot(in fileballot.v):

Theorem bertrand_ballot p q :
  let l := filter (fun votes => count_votes votes "A" =? p) (picks (p + q) ["A"; "B"]) in
  p >= q ->
  (p + q) * List.length (filter (throughout (wins "A" "B")) l) =
  (p - q) * List.length (filter (wins "A" "B") l).

The Coq development team(in standard library, Sets/Image and Sets/Infinite_sets ):

Theorem Pigeonhole :
  forall (A:Ensemble U) (f:U -> V) (n:nat),
    cardinal U A n ->
    forall n':nat, cardinal V (Im A f) n' -> n' < n -> ~ injective f.

Lemma Pigeonhole_principle :
  forall (A:Ensemble U) (f:U -> V) (n:nat),
    cardinal _ A n ->
    forall n':nat,
      cardinal _ (Im A f) n' ->
      n' < n ->  exists x : _, (exists y : _, f x = f y /\ x <> y).

Theorem Pigeonhole_bis :
  forall (A:Ensemble U) (f:U -> V),
    ~ Finite U A -> Finite V (Im U V A f) -> ~ injective U V f.

Theorem Pigeonhole_ter :
  forall (A:Ensemble U) (f:U -> V) (n:nat),
    injective U V f -> Finite V (Im U V A f) -> Finite U A.

constructive version (the proof from the standard library uses excluded middle)

Theorem pigeonhole :
  forall m n, m < n -> forall f, (forall i, f i < m) ->
    { i : nat & { j : nat | i < j < n /\ f i = f j } }.

Theorem ramsey A (W : set A) n (P : Pinf W) B : forall (C : Pf B)
  (f : Pcard P (S n) -> elts C), Proper (Pcard_equiv ==> elts_eq) f ->
  exists c (Q : Pinf P), forall X : Pcard Q (S n), f (Pcard_subset Q X) = c.

Georges Gonthier, Benjamin Werner(on github ):

Theorem four_color : forall m : map R, simple_map m -> map_colorable 4 m.

Coqtail (Coqtail/Reals/Rseries/Rseries_RiemannInt) :

Lemma harmonic_series_equiv : (sum_f_R0 (fun n ⇒ / (S n))) ~ (fun n ⇒ ln (S (S n))).

Luís Cruz-Filipe(in C-CoRN/ftc/Taylor ):

Theorem Taylor : forall e, Zero [<] e -> forall Hb',
  {c : IR | Compact (Min_leEq_Max a b) c |
    forall Hc, AbsIR (F b Hb'[-]Part _ _ Taylor_aux[-]deriv_Sn c Hc[*] (b[-]a)) [<=] e}.

Frédéric Chardard(in file37.cardan3.v):

Theorem Cardan_Tartaglia : forall a1 a2 a3 :C,
    let s := -a1 / 3 in
    let p := a2 + 2 * s * a1 + 3 * pow s 2 in
    let q := a3 + a2 * s + a1 * pow s 2 + pow s 3 in
    (p <> 0 ->
     let Delta := pow (q / 2) 2 + pow (p / 3) 3 in
     let alpha := cubicroot (- (q / 2) + nroot 2 Delta) in
     let beta := - (p / 3) / alpha in
     let z1 := alpha + beta in
     let z2 := alpha * CJ + beta * pow CJ 2 in
     let z3 := alpha * pow CJ 2 + beta * CJ in
     forall u : C,
       (u - (s + z1)) * (u - (s + z2)) * (u - (s + z3))
       = pow u 3 + a1 * pow u 2 + a2 * u + a3)
    /\
    (p = 0 ->
     let z1 := - cubicroot q in
     let z2 := z1 * CJ in
     let z3 := z1 * pow CJ 2 in
     forall u : C,
       (u - (s + z1)) * (u - (s + z2)) * (u - (s + z3))
       = pow u 3 + a1 * pow u 2 + a2 * u + a3).

Jean-Marie Madiot(in filemean.v, using forward-backward induction):

Theorem geometric_arithmetic_mean (a : nat -> R) (n : nat) :
  n <> O ->
  (forall i, (i < n)%nat -> 0 <= a i) ->
  prod n a <= (sum n a / INR n) ^ n
  /\
  (prod n a = (sum n a / INR n) ^ n -> forall i, (i < n)%nat -> a i = a O).

Daniel de Rauglaudre(on gforge (use login anonsvn / anonsvn if needed)):

Theorem puiseux_series_algeb_closed : ∀ (α : Type) (R : ring α) (K : field R),
  algeb_closed_field K
  → ∀ pol : polynomial (puiseux_series α),
    degree (ps_zerop K) pol ≥ 1
    → ∃ s : puiseux_series α, (ps_pol_apply pol s = 0)%ps.

Coqtail(in Coqtail/Reals/Triangular ):

Lemma sum_reciprocal_triangular : Rser_cv (fun n => / triangle (S n)) 2.

The Coq development team(in standard library, Reals/Binomial ):

For the non-constructive type R

Lemma binomial :
  forall (x y:R) (n:nat),
    (x + y) ^ n = sum_f_R0 (fun i:nat => C n i * x ^ i * y ^ (n - i)) n.

For the type nat

Theorem exp_Pascal :
 forall a b n : nat,
 power (a + b) n =
 sum_nm n 0 (fun k : nat => binomial n k * (power a (n - k) * power b k)).

For any commutative ring X.

Definition newton_sum n a b : X :=
  CRsum (fun k => (Nbinomial n k) ** (a ^ k) * (b ^ (n - k))) n.

Theorem Newton : forall n a b, (a + b) ^ n == newton_sum n a b.

Sidi Ould Biha(in mathcomp/algebra/mxpoly ):

Theorem Cayley_Hamilton (R : comRingType) n' (A : 'M[R]_n'.+1) :
  horner_mx A (char_poly A) = 0.

unknown (Inria, Microsoft)(in mathcomp/ssreflect/binomial ):

copyrighted:

(c) Copyright Microsoft Corporation and Inria. All rights reserved.

Theorem Wilson : forall p, p > 1 -> prime p = (p %| ((p.-1)`!).+1).

licence: LGPL

Theorem wilson: forall p, prime p ->  Zis_mod (Zfact (p - 1)) (- 1) p.

unknown (Inria, Microsoft)(in mathcomp/ssreflect/finset ):

Lemma card_powerset (T : finType) (A : {set T}) : #|powerset A| = 2 ^ #|A|.

Lemma powerset_cardinal:
  forall s, MM.cardinal (powerset s) = two_power (M.cardinal s).

Sophie Bernard and Laurence Rideau () :

The concept algebraicOver is available from the public release ssreflect-1.4, ratr is the type of rational numbers. The definition of PI is from the Coq standard library.

Theorem pi_transcendant : ~ (algebraicOver ratr (PI)%:C).

Jean-Marie Madiot(in filekonigsberg_bridges.v):

Theorem konigsberg_bridges :
  let E := [(0, 1); (0, 2); (0, 3); (1, 2); (1, 2); (2, 3); (2, 3)] in
  forall p, path p -> eulerian E p -> False.

Loïc Pottier, Benjamin Grégoire, Laurent Théry(in CertiGeo/chords ):

The proof uses just two tactics. The first one transforms the goal into an algebraic statement and the second one generates and then checks a proof certificate.

More information here: http://hal.inria.fr/inria-00504719_v1/

Lemma chords: forall O A B C D M:point,
  equaldistance O A O B ->
  equaldistance O A O C ->
  equaldistance O A O D ->
  collinear A B M -> collinear C D M ->
  scalarproduct A M B = scalarproduct C M D
  \/ parallel A B C D.

Sophie Bernard(on github . See installation instructions ):

Theorem HermiteLindemann (x : complexR) :
  x != 0 -> x is_algebraic -> ~ ((Cexp x) is_algebraic).

Julien Narboux(in AreaMethod/pythagoras_difference_lemmas ):

Definition Py A B C := A**B * A**B + B**C * B**C - A**C * A**C.

Lemma herron_qin : forall A B C,
  S A B C * S A B C = 1 / (2*2*2*2) * (Py A B A * Py A C A - Py B A C * Py B A C).

Pierre Letouzey(in contribs/FSets/PowerSet ):

Lemma powerset_k_cardinal : forall s k, 
  MM.cardinal (powerset_k s k) = binomial (M.cardinal s) k.

The Coq development team(in standard library, ZArith/Znumtheory ):

Inductive Zdivide (a b:Z) : Prop :=
    Zdivide_intro : forall q:Z, b = q * a -> Zdivide a b.

Notation "( a | b )" := (Zdivide a b) (at level 0) : Z_scope.

Inductive Zis_gcd (a b d:Z) : Prop :=
  Zis_gcd_intro :
  (d | a) ->
  (d | b) ->
  (forall x:Z, (x | a) -> (x | b) -> (x | d)) ->
    Zis_gcd a b d.

Inductive Bezout (a b d:Z) : Prop :=
  Bezout_intro : forall u v:Z, u * a + v * b = d -> Bezout a b d.

Lemma Zis_gcd_bezout : forall a b d:Z, Zis_gcd a b d -> Bezout a b d.

Julien Narboux(in contribs/AreaMethod/examples_2 ):

Theorem Ceva :
 forall A B C D E F G P : Point,
 inter_ll D B C A P ->
 inter_ll E A C B P ->
 inter_ll F A B C P ->
 F <> B ->
 D <> C ->
 E <> A ->
 parallel A F F B ->
 parallel B D D C ->
 parallel C E E A ->
 (A ** F / F ** B) * (B ** D / D ** C) * (C ** E / E ** A) = 1.

Gilles Kahn, Gerard Huet(in standard library, Sets/Powerset.v ):

"Naive Set Theory in Coq"

Theorem Strict_Rel_is_Strict_Included :
 same_relation (Ensemble U) (Strict_Included U)
   (Strict_Rel_of (Ensemble U) (Power_set_PO (Full_set U))).

Sylvain Dailler (Coqtail)(in Coqtail/Reals/Hopital ):

Many other versions in the file, for example depending on whether the limits are finite or not.

Variables f g : R → R.
Variables a b L : R.
Hypothesis Hab : a < b.
Hypotheses (Df : ∀ x, open_interval a b x → derivable_pt f x)
           (Dg : ∀ x, open_interval a b x → derivable_pt g x).
Hypotheses (Cf : ∀ x, a ≤ x ≤ b → continuity_pt f x)
           (Cg : ∀ x, a ≤ x ≤ b → continuity_pt g x).
Hypothesis (Zf : limit1_in f (open_interval a b) 0 a).
Hypothesis (Zg : limit1_in g (open_interval a b) 0 a).

Hypothesis (g_not_0 : ∀ x (Hopen: open_interval a b x), derive_pt g x (Dg x Hopen) ≠ 0 ∧ g x ≠ 0)
Hypothesis (Hlimder : ∀ eps, eps > 0 →
  ∃ alp,
    alp > 0 ∧
    (∀ x (Hopen : open_interval a b x), R_dist x a < alp →
      R_dist (derive_pt f x (Df x Hopen) / derive_pt g x (Dg x Hopen)) L < eps)).

Theorem Hopital_g0_Lfin_right : limit1_in (fun x ⇒ f x / g x) (open_interval a b) L a.

Frédérique Guilhot(in contribs/HighSchoolGeometry/isocele ):

Lemma isocele_angles_base :
 isocele A B C -> cons_AV (vec B C) (vec B A) = cons_AV (vec C A) (vec C B).

GeoCoq team (GeoCoq in triangle.v ) :

Lemma isosceles_conga :
  A<>C -> A <> B ->
  isosceles A B C ->
  Conga C A B A C B.

Luís Cruz-Filipe(in C-CoRN/ftc/MoreFunSeries ):

Lemma fun_power_series_conv_IR :
  fun_series_convergent_IR
  (olor ([--][1]) [1])
  (fun (i:nat) => Fid IR{^}i).

Sophie Bernard and Laurence Rideau () :

The concept algebraicOver is available from the public release ssreflect-1.4, ratr is the type of rational numbers. The definition of exp is from the Coq standard library.

Theorem e_transcendant : ~ (algebraicOver ratr (exp 1)%:C).

many versions(e.g. file68.sumarith.v):

Theorem arith_sum a b n : 2 * sum (fun i => a + i * b) n = S n * (2 * a + n * b).

The Coq development team(in standard library, ZArith/Znumtheory ):

This is a binary version, as it is more efficient in coq.

(There are several other versions in this file)

Fixpoint Pgcdn (n: nat) (a b : positive) : positive :=
  match n with
    | O => 1
    | S n =>
      match a,b with
	| xH, _ => 1
	| _, xH => 1
	| xO a, xO b => xO (Pgcdn n a b)
	| a, xO b => Pgcdn n a b
	| xO a, b => Pgcdn n a b
	| xI a', xI b' =>
          match Pcompare a' b' Eq with
	    | Eq => a
	    | Lt => Pgcdn  n (b'-a') a
	    | Gt => Pgcdn n (a'-b') b
          end
      end
  end.

Definition Zgcd (a b : Z) : Z :=
  match a,b with
    | Z0, _ => Zabs b
    | _, Z0 => Zabs a
    | Zpos a, Zpos b => Zpos (Pgcd a b)
    | Zpos a, Zneg b => Zpos (Pgcd a b)
    | Zneg a, Zpos b => Zpos (Pgcd a b)
    | Zneg a, Zneg b => Zpos (Pgcd a b)
  end.

Lemma Zgcd_is_gcd : forall a b, Zis_gcd a b (Zgcd a b).

unknown (Laurent Théry?)(in mathcomp/fingroup/fingroup ):

Theorem Lagrange G H : H \subset G -> (#|H| * #|G : H|)%N = #|G|.

Laurent Théry(in mathcomp/solvable/sylow ):

Theorem Sylow's_theorem :
  [/\ forall P, [max P | p.-subgroup(G) P] = p.-Sylow(G) P,
      [transitive G, on 'Syl_p(G) | 'JG],
      forall P, p.-Sylow(G) P -> #|'Syl_p(G)| = #|G : 'N_G(P)|
   &  prime p -> #|'Syl_p(G)| %% p = 1%N].

Florent Hivert( on Github ):

Variable T : ordType. (* a totally ordered type *)
(*   <= is denoted (leqX T)       *)
(*   >  is denoted (gtnX T)       *)

Theorem Erdos_Szekeres (m n : nat) (s : seq T) :
  (size s) > (m * n) ->
  (exists t, subseq t s /\ sorted (leqX T) t /\ size t > m) \/
  (exists t, subseq t s /\ sorted (gtnX T) t /\ size t > n).

built-in(definition of natural numbers in Coq's standard library: Coq/Init/Datatypes ):

This is automatically deduced by coq when defining the set of natural numbers. This lemma is inhabited by the following term:

fun P HO HS => fix f n : P n := match n with O => HO | S p => HS p (f p) end

Inductive nat : Set :=  O : nat | S : nat -> nat.

Lemma nat_ind :
  forall P : nat -> Prop,
  P 0 ->
  (forall n : nat, P n -> P (S n)) ->
  forall n : nat, P n.

Luís Cruz-Filipe(in C-CoRN/ftc/Rolle ):

Theorem Law_of_the_Mean : forall a b, I a -> I b -> forall e, Zero [<] e ->
 {x : IR | Compact (Min_leEq_Max a b) x | forall Ha Hb Hx,
  AbsIR (F b Hb[-]F a Ha[-]F' x Hx[*] (b[-]a)) [<=] e}.

Daniel de Rauglaudre(in roglo/cauchy_schwarz ):

Notation "'Σ' ( i = b , e ) , g" := (summation b e (λ i, (g)%R)).
Notation "u .[ i ]" := (List.nth (pred i) u 0%R).
Cauchy_Schwarz_inequality
     : ∀ (u v : list R) (n : nat),
       (Σ (k = 1, n), (u.[k] * v.[k])²
        ≤ Σ (k = 1, n), ((u.[k])²) * Σ (k = 1, n), ((v.[k])²))%R

The Coq development team(in Coq's standard library: Reals/Rsqrt_def ):

(non constructive version)

Lemma IVT_cor :
  forall (f:R -> R) (x y:R),
    continuity f ->
    x <= y -> f x * f y <= 0 ->
    { z:R | x <= z <= y /\ f z = 0 }.

unknown (Inria, Microsoft)( ssreflect/prime ):

Lemma divisors_correct : forall n, n > 0 ->
  [/\ uniq (divisors n), sorted leq (divisors n)
    & forall d, (d \in divisors n) = (d %| n)].

Theorem Morley:
 forall (a b c : R) (A B C P Q T : PO),
 0 < a ->
 0 < b ->
 0 < c ->
 (a + b) + c = pisurtrois ->
 A <> B ->
 A <> C ->
 B <> C ->
 B <> P ->
 B <> Q ->
 A <> T ->
 C <> T ->
 image_angle b = cons_AV (vec B C) (vec B P) ->
 image_angle b = cons_AV (vec B P) (vec B Q) ->
 image_angle b = cons_AV (vec B Q) (vec B A) ->
 image_angle c = cons_AV (vec C P) (vec C B) ->
 image_angle c = cons_AV (vec C T) (vec C P) ->
 image_angle a = cons_AV (vec A B) (vec A Q) ->
 image_angle a = cons_AV (vec A Q) (vec A T) ->
 image_angle a = cons_AV (vec A T) (vec A C) ->  equilateral P Q T.

many versions ( local ) :

Theorem div3 : forall n d,
  (number n d) mod 3 = (sumdigits n d) mod 3.

Frédérique Guilhot(in contribs/HighSchoolGeometry/affine_classiques ):

Theorem Desargues :
 forall A B C A1 B1 C1 S : PO,
 C <> C1 -> B <> B1 -> C <> S -> B <> S -> C1 <> S ->
 B1 <> S -> A1 <> B1 -> A1 <> C1 -> B <> C -> B1 <> C1 ->
 triangle A A1 B ->
 triangle A A1 C ->
 alignes A A1 S ->
 alignes B B1 S ->
 alignes C C1 S ->
 paralleles (droite A B) (droite A1 B1) ->
 paralleles (droite A C) (droite A1 C1) ->
 paralleles (droite B C) (droite B1 C1).

Proved with the area_method tactic.
http://dpt-info.u-strasbg.fr/~narboux/area_method.html

Theorem Desargues :
 forall A B C X A' B' C' : Point, A' <>C' -> A' <> B' ->
 on_line A' X A ->
 on_inter_line_parallel B' A' X B A B ->
 on_inter_line_parallel C' A' X C A C ->
 parallel B C B' C'.

Gabriel Braun( GeoCoq/Ch13_6_Desargues_Hessenberg ):

Hessenberg's proof following the book of Tarski.

Lemma l13_15 : forall A B C A' B' C' O ,
  ~Col A B C ->
  Par_strict A B A' B' ->
  Par_strict A C A' C' ->
  Col O A A' ->
  Col O B B' ->
  Col O C C' ->
  Par B C B' C'.

Lemma l13_18 : forall A B C A' B' C' O,
  ~Col A B C /\ Par_strict A B A' B' /\  Par_strict A C A' C' ->
  (Par_strict B C B' C' /\ Col O A A' /\ Col O B B' -> Col O C C') /\
  ((Par_strict B C B' C' /\ Par A A' B B') ->
  (Par C C' A A' /\ Par C C' B B'))  /\
  (Par A A' B B' /\ Par A A' C C' -> Par B C B' C').

unknown ((c) Microsoft Corporation and Inria)( math-comp/algebra/polydiv ):

CoInductive edivp_spec m d : nat * {poly F} * {poly F} -> Type :=
  EdivpSpec n q r of
  m = q * d + r & (d != 0) ==> (size r < size d) : edivp_spec m d (n, q, r).

Lemma edivpP m d : edivp_spec m d (edivp m d).

Coqtail team( Coqtail/Reals/RStirling ):

Lemma Stirling_equiv :
  Rseq_fact ~ (fun n => sqrt (2 × PI) × (INR n) ^ n × exp (- (INR n)) × sqrt (INR n)).

The Coq Development Team(in standard library, Reals/Rgeom ):

Lemma triangle :
  forall x0 y0 x1 y1 x2 y2:R,
    dist_euc x0 y0 x1 y1 <= dist_euc x0 y0 x2 y2 + dist_euc x2 y2 x1 y1.

Jean-Marie Madiot(in filebirthday.v):

Note: this formalization uses lists of natural numbers to model sets.

Theorem birthday_paradox :
  let l := picks 23 (enumerate 365) in
  2 * length (filter collision l) > length l.

Theorem birthday_paradox_min :
  let l := picks 22 (enumerate 365) in
  2 * length (filter collision l) < length l.

Frédérique Guilhot(in contribs/HighSchoolGeometry/metrique_triangle ):

Theorem Al_Kashi :
 forall (A B C : PO) (a : R),
 A <> B ->
 A <> C ->
 image_angle a = cons_AV (vec A B) (vec A C) ->
 Rsqr (distance B C) =
 Rsqr (distance A B) + Rsqr (distance A C) -
 2 * distance A B * distance A C * cos a.

Tuan Minh Pham ( link to the publication on HAL ):

forall (O A B C D : PO) (r: R),
convexQuad A B C D ? concyclic O r A B C D ?
AD ? BC + AB ? CD = AC ? BD.

Jean-Marie Madiot(in fileinclusionexclusion.v):

Theorem inclusion_exclusion (l : list set) :
  cardinal (list_union l) =
  sum
    (map (fun l' => cardinal (list_intersection l') *
                 alternating_sign (1 + length l'))
         (filter nonempty (sublists l))).

Georges Gonthier et al.( coqfinitgroup/matrix ):

Lemma mul_mx_adj : forall n (A : 'M[R]_n), A *m \adj A = (\det A)%:M.

Lemma trmx_adj : forall n (A : 'M[R]_n), (\adj A)^T = \adj A^T.

Lemma mul_adj_mx : forall n (A : 'M[R]_n), \adj A *m A = (\det A)%:M.

Laurent Théry(in contribs/Bertrand/Bertrand ):

Theorem Bertrand :
 forall n : nat, 2 <= n -> exists p : nat, prime p /\ n < p /\ p < 2 * n.