added a function to reorder the metasenv.

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

diff --git a/helm/matita/library/nat/primes.ma b/helm/matita/library/nat/primes.ma
index d7ee89d4e5490fb2736c8b50597600927c137ac1..644cae978f58a419e9d2d53ca2188b7fbcbe1322 100644 (file)
--- a/helm/matita/library/nat/primes.ma
+++ b/helm/matita/library/nat/primes.ma
@@ -116,10 +116,11 @@ apply lt_O_n_elim n2 Hcut.intro.rewrite < sym_times.
 simplify.rewrite < sym_plus.
 apply le_plus_n.
 elim le_to_or_lt_eq O n2.
-assumption.apply le_O_n.
+assumption.
 absurd O<m.assumption.
 rewrite > H2.rewrite < H3.rewrite < times_n_O.
 apply not_le_Sn_n O.
+apply le_O_n.
 qed.
 
 theorem divides_to_lt_O : \forall n,m. O < m \to divides n m \to O < n.