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

### 2. Fundamental Theorem of Algebra

(in C-CoRN/fta/FTA):

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

### 3. The Denumerability of the Rational Numbers

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

(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

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

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

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

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

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

(in cocorico, compatible with coq 7.3):

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

No known statement.

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

(in Coqtail/Reals/Rzeta2):

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

(in C-CoRN/ftc/FTC):

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

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

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

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

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

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


(in C-CoRN/reals/RealCount):
Theorem reals_not_countable : forall (f : nat -> IR), {x :IR | forall n : nat, x [#] (f n)}.


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

(in contribs/Schroeder/Schroeder):

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

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

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

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

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


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


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

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

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


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


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

(on github):

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

No known statement.

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

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


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

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

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

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

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

(in mathcomp/ssreflect/finset):

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

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

():

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

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


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

(on github. See installation instructions):

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


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


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

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

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

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

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


(in C-CoRN/ftc/MoreFunSeries):

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


():

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


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

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

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

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

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

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

(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


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


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

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


(local):

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


No known statement.

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

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

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

(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/Reals/RStirling):

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

No known statement.

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


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

):

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.

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


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

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