X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2Flibrary%2Fnat%2Flt_arith.ma;h=f60da5eba31f2c07d7b53c70d62c231d362c2208;hb=771ee8b9d122fa963881c876e86f90531bb7434f;hp=b8339f374e6019dd054719c9928bf735c63aef4b;hpb=400b07e007cfbb0b4ce5ed77cfc50f227c491310;p=helm.git

diff --git a/helm/matita/library/nat/lt_arith.ma b/helm/matita/library/nat/lt_arith.ma
index b8339f374..f60da5eba 100644
--- a/helm/matita/library/nat/lt_arith.ma
+++ b/helm/matita/library/nat/lt_arith.ma
@@ -204,10 +204,14 @@ monotonic nat lt f \to injective nat nat f.
 unfold injective.intros.
 apply (nat_compare_elim x y).
 intro.apply False_ind.apply (not_le_Sn_n (f x)).
-rewrite > H1 in \vdash (? ? %).apply H.apply H2.
+rewrite > H1 in \vdash (? ? %).
+change with (f x < f y).
+apply H.apply H2.
 intros.assumption.
 intro.apply False_ind.apply (not_le_Sn_n (f y)).
-rewrite < H1 in \vdash (? ? %).apply H.apply H2.
+rewrite < H1 in \vdash (? ? %).
+change with (f y < f x).
+apply H.apply H2.
 qed.
 
 theorem increasing_to_injective: \forall f:nat\to nat.