X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Flibrary%2Fnat%2Fchinese_reminder.ma;h=31b976dcf4abd98169bd73a39068ba172871889c;hb=c3bba4af040f8040e5eae07e70690c52f8c614f8;hp=30cc7440f8a723d99fc1b6cd8371ce5bdbcf1931;hpb=7f2444c2670cadafddd8785b687ef312158376b0;p=helm.git

diff --git a/matita/library/nat/chinese_reminder.ma b/matita/library/nat/chinese_reminder.ma
index 30cc7440f..31b976dcf 100644
--- a/matita/library/nat/chinese_reminder.ma
+++ b/matita/library/nat/chinese_reminder.ma
@@ -215,14 +215,11 @@ 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