Complete proof of Bertrand for n >= 256.

[helm.git] / helm / software / matita / library / nat / gcd.ma

diff --git a/helm/software/matita/library/nat/gcd.ma b/helm/software/matita/library/nat/gcd.ma
index ded9d4843ac6cf3cb4da2b4f564568db2df2e02b..3db29f622fb95a5e096cb46744928c97bcef9f39 100644 (file)
--- a/helm/software/matita/library/nat/gcd.ma
+++ b/helm/software/matita/library/nat/gcd.ma
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/gcd".
-
 include "nat/primes.ma".
 include "nat/lt_arith.ma".
 
@@ -101,7 +99,6 @@ qed.
 theorem divides_gcd_nm: \forall n,m.
 gcd n m \divides m \land gcd n m \divides n.
 intros.
-(*CSC: simplify simplifies too much because of a redex in gcd *)
 change with
 (match leb n m with
   [ true \Rightarrow 
@@ -594,7 +591,6 @@ intro.apply (nat_case n)
 qed.
 
 theorem symmetric_gcd: symmetric nat gcd.
-(*CSC: bug here: unfold symmetric does not work *)
 change with 
 (\forall n,m:nat. gcd n m = gcd m n).
 intros.
@@ -749,6 +745,7 @@ apply gcd_O_to_eq_O.apply sym_eq.assumption.
 apply le_to_or_lt_eq.apply le_O_n.
 qed.
 
+(* primes and divides *)
 theorem divides_times_to_divides: \forall n,p,q:nat.prime n \to n \divides p*q \to
 n \divides p \lor n \divides q.
 intros.
@@ -802,6 +799,30 @@ cut (n \divides p \lor n \ndivides p)
   ]
 qed.
 
+theorem divides_exp_to_divides: 
+\forall p,n,m:nat. prime p \to 
+p \divides n \sup m \to p \divides n.
+intros 3.elim m.simplify in H1.
+apply (transitive_divides p (S O)).assumption.
+apply divides_SO_n.
+cut (p \divides n \lor p \divides n \sup n1).
+elim Hcut.assumption.
+apply H.assumption.assumption.
+apply divides_times_to_divides.assumption.
+exact H2.
+qed.
+
+theorem divides_exp_to_eq: 
+\forall p,q,m:nat. prime p \to prime q \to
+p \divides q \sup m \to p = q.
+intros.
+unfold prime in H1.
+elim H1.apply H4.
+apply (divides_exp_to_divides p q m).
+assumption.assumption.
+unfold prime in H.elim H.assumption.
+qed.
+
 theorem eq_gcd_times_SO: \forall m,n,p:nat. O < n \to O < p \to
 gcd m n = (S O) \to gcd m p = (S O) \to gcd m (n*p) = (S O).
 intros.
@@ -877,4 +898,37 @@ cut (n \divides p \lor n \ndivides p)
  |apply (decidable_divides n p).
   assumption.
  ]
+qed.
+
+(*
+theorem divides_to_divides_times1: \forall p,q,n. prime p \to prime q \to p \neq q \to
+divides p n \to divides q n \to divides (p*q) n.
+intros.elim H3.
+rewrite > H5 in H4.
+elim (divides_times_to_divides ? ? ? H1 H4)
+  [elim H.apply False_ind.
+   apply H2.apply sym_eq.apply H8
+    [assumption
+    |apply prime_to_lt_SO.assumption
+    ]
+  |elim H6.
+   apply (witness ? ? n1).
+   rewrite > assoc_times.
+   rewrite < H7.assumption
+  ]
+qed.
+*)
+
+theorem divides_to_divides_times: \forall p,q,n. prime p  \to p \ndivides q \to
+divides p n \to divides q n \to divides (p*q) n.
+intros.elim H3.
+rewrite > H4 in H2.
+elim (divides_times_to_divides ? ? ? H H2)
+  [apply False_ind.apply H1.assumption
+  |elim H5.
+   apply (witness ? ? n1).
+   rewrite > sym_times in ⊢ (? ? ? (? % ?)).
+   rewrite > assoc_times.
+   rewrite < H6.assumption
+  ]
 qed.
\ No newline at end of file