Added lt_O_S.

[helm.git] / helm / software / matita / library / nat / totient.ma

diff --git a/helm/software/matita/library/nat/totient.ma b/helm/software/matita/library/nat/totient.ma
index 24c3920ed82571324c2977a7be798b492fbf43e7..2c6061e0b80c673158812a259d0e944280d0a8f6 100644 (file)
--- a/helm/software/matita/library/nat/totient.ma
+++ b/helm/software/matita/library/nat/totient.ma
@@ -44,8 +44,7 @@ apply (count_times m m2 ? ? ?
 intros.unfold cr_pair.
 apply (le_to_lt_to_lt ? (pred ((S m)*(S m2)))).
 unfold min.
-apply le_min_aux_r.
-change with ((S (pred ((S m)*(S m2)))) \le ((S m)*(S m2))).
+apply le_min_aux_r.unfold lt.
 apply (nat_case ((S m)*(S m2))).apply le_n.
 intro.apply le_n.
 intros.