Complete proof of Bertrand for n >= 256.

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

diff --git a/helm/software/matita/library/nat/chinese_reminder.ma b/helm/software/matita/library/nat/chinese_reminder.ma
index 30cc7440f8a723d99fc1b6cd8371ce5bdbcf1931..2bf3bc59e0d95c00510e827371b9eac04a453d1e 100644 (file)
--- a/helm/software/matita/library/nat/chinese_reminder.ma
+++ b/helm/software/matita/library/nat/chinese_reminder.ma
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/chinese_reminder".
-
 include "nat/exp.ma".
 include "nat/gcd.ma".
 include "nat/permutation.ma".
@@ -215,25 +213,23 @@ generalize in match Hcut.
 apply andb_elim.
 apply eqb_elim.intro.
 rewrite > H3.
-change with 
-(eqb ((cr_pair m n a b) \mod n) b = true \to 
-a = a \land (cr_pair m n a b) \mod n = b).
+simplify.
 intro.split.reflexivity.
 apply eqb_true_to_eq.assumption.
 intro.
-change with (false = true \to 
-(cr_pair m n a b) \mod m = a \land (cr_pair m n a b) \mod n = b).
+simplify.
 intro.apply False_ind.
 apply not_eq_true_false.apply sym_eq.assumption.
 apply (f_min_aux_true 
-(\lambda x. andb (eqb (x \mod m) a) (eqb (x \mod n) b)) (pred (m*n)) (pred (m*n))).
+(\lambda x. andb (eqb (x \mod m) a) (eqb (x \mod n) b)) (pred (m*n)) O).
 elim (and_congruent_congruent_lt m n a b).
 apply (ex_intro ? ? a1).split.split.
-rewrite < minus_n_n.apply le_O_n.
+apply le_O_n.
 elim H3.apply le_S_S_to_le.apply (trans_le ? (m*n)).
 assumption.apply (nat_case (m*n)).apply le_O_n.
 intro.
-rewrite < pred_Sn.apply le_n.
+rewrite < pred_Sn.
+rewrite < plus_n_O.apply le_n.
 elim H3.elim H4.
 apply andb_elim.
 cut (a1 \mod m = a).