X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fchinese_reminder.ma;h=766b85f715324398d2cde65bddf9c96f3c8da90c;hb=34d2f477be65e3fd26bfb6d43a3dd0807274549b;hp=31b976dcf4abd98169bd73a39068ba172871889c;hpb=ebb14e0084aecd167bc42245625c4eb3167df9d5;p=helm.git

diff --git a/helm/software/matita/library/nat/chinese_reminder.ma b/helm/software/matita/library/nat/chinese_reminder.ma
index 31b976dcf..766b85f71 100644
--- a/helm/software/matita/library/nat/chinese_reminder.ma
+++ b/helm/software/matita/library/nat/chinese_reminder.ma
@@ -223,14 +223,15 @@ 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).