New reduction strategy (that behaves much better during simplification).

[helm.git] / helm / matita / library / nat / lt_arith.ma

diff --git a/helm/matita/library/nat/lt_arith.ma b/helm/matita/library/nat/lt_arith.ma
index b8339f374e6019dd054719c9928bf735c63aef4b..f60da5eba31f2c07d7b53c70d62c231d362c2208 100644 (file)
--- 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.