X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fchinese_reminder.ma;h=30cc7440f8a723d99fc1b6cd8371ce5bdbcf1931;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=f14f16d2792c3f2d291db23ee8d4586d9520df01;hpb=b3f74fab711510628cff64aff3e48e73cc9f6e09;p=helm.git

diff --git a/helm/matita/library/nat/chinese_reminder.ma b/helm/matita/library/nat/chinese_reminder.ma
index f14f16d27..30cc7440f 100644
--- a/helm/matita/library/nat/chinese_reminder.ma
+++ b/helm/matita/library/nat/chinese_reminder.ma
@@ -53,7 +53,7 @@ apply minus_to_plus.
 apply lt_to_le.
 change with (O + a2*m < a1*n).
 apply lt_minus_to_plus.
-rewrite > H5.simplify.apply le_n.
+rewrite > H5.unfold lt.apply le_n.
 assumption.
 (* congruent to b *)
 cut (a2*m = a1*n - (S O)).
@@ -84,7 +84,7 @@ apply minus_to_plus.
 apply lt_to_le.
 change with (O + a2*m < a1*n).
 apply lt_minus_to_plus.
-rewrite > H5.simplify.apply le_n.
+rewrite > H5.unfold lt.apply le_n.
 assumption.
 (* and now the symmetric case; the price to pay for working
    in nat instead than Z *)
@@ -119,7 +119,7 @@ apply minus_to_plus.
 apply lt_to_le.
 change with (O + a1*n < a2*m).
 apply lt_minus_to_plus.
-rewrite > H5.simplify.apply le_n.
+rewrite > H5.unfold lt.apply le_n.
 assumption.
 (* congruent to a *)
 cut (a2*m = a1*n + (S O)).
@@ -149,7 +149,7 @@ apply minus_to_plus.
 apply lt_to_le.
 change with (O + a1*n < a2*m).
 apply lt_minus_to_plus.
-rewrite > H5.simplify.apply le_n.
+rewrite > H5.unfold lt.apply le_n.
 assumption.
 (* proof of the cut *)
 rewrite < H2.