Formalizing 100 theorems in Coq


This is an appendix to Freek Wiedijk's webpage on the "top 100" mathematical theorems, to keep track of the statements of the theorems that are formalised in Coq. Drop me or Freek an email or make a pull request if you have updates.

1. The Irrationality of the Square Root of 2

2. Fundamental Theorem of Algebra

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

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

3. The Denumerability of the Rational Numbers

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 }}.

Daniel Schepler (in contribs/ZornsLemma/CountableTypes):
Inductive CountableT (X:Type) : Prop := | intro_nat_injection: forall f:X->nat, injective f -> CountableT X. Lemma Q_countable: CountableT Q.

4. Pythagorean Theorem

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):

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.

5. Prime Number Theorem

No known statement.

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 (in contribs/Goedel/goedel2):
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)).

No known statement.

No known statement.

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

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

No known statement.

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

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}.

The Coq development team (in standard library, Reals/RiemannInt):
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.

No known statement.

Coqtail team (in Coqtail/Complex/Cexp):

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.

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

Theorem lagrange_4_square_theorem : forall n, 0 <=> { 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 <=> (forall p, prime p -> Zis_mod p 3 4 -> Zeven (Zdiv_exp p n)) -> sum_of_two_squares n.

No known statement.

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 <=>

C-CoRN team (in C-CoRN/reals/RealCount):
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 <=>

No known statement.

Hugo Herbelin (in contribs/Schroeder/Schroeder):

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

Daniel Schepler (in contribs/ZornsLemma/CSB):
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 <=> 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.

Luís Cruz-Filipe (in C-CoRN/transc/MoreArcTan):
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):

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 file ballot.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.

Jean-Marie Madiot (many versions by others) (pigeonhole.v):
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 } }.
Frédéric Blanqui (in CoLoR/Util/Set/Ramsey):
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.

No known statement.

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

Theorem Taylor : forall e, Zero [<]> 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)) [<=]>

No known statement.

Frédéric Chardard (in file 37.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 file mean.v, using forward-backward induction):

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

No known statement.

No known statement.

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.

No known statement.

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

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.

Laurent Thery & Jose C. Almeida (in contribs/RSA/Binomials):
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)).
Jean-Marie Madiot (in Coqtail/Hierarchy/Commutative_ring_binomial):
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.

No known statement.

No known statement.

No known statement.

No known statement.

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.

No known statement.

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

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

Pierre Letouzey (in contribs/FSets/PowerSet):
Lemma powerset_cardinal: forall s, MM.cardinal (powerset s) = two_power (M.cardinal s).

Sophie Bernard and Laurence Rideau ():

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

Jean-Marie Madiot (in file konigsberg_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):

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.

No known statement.

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.

No known statement.

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

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):

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.

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 ():

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

many versions (e.g. file 68.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):

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).

No known statement.

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 (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):

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 [<]> {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)) [<=]>

No known statement.

No known statement.

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):

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

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)].

No known statement.

No known statement.

No known statement.

Frédérique Guilhot (on Github: HighSchoolGeometry/exercice_morley):
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.

No known statement.

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).

Julien Narboux (in contribs/AreaMethod/examples_2):
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):

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').

No known statement.

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)).

No known statement.

Jean-Marie Madiot (in file birthday.v):

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 file inclusionexclusion.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 <=> exists p : nat, prime p /\ n < p /\ p < 2 * n.

No known statement.

No known statement.