added a function to reorder the metasenv.

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

diff --git a/helm/matita/library/nat/nth_prime.ma b/helm/matita/library/nat/nth_prime.ma
index 5ff937e42b139a94f281cddb19aa6872a968ba2f..ee21195dc10bd823f4a96b8998a87ad99f6bb562 100644 (file)
--- a/helm/matita/library/nat/nth_prime.ma
+++ b/helm/matita/library/nat/nth_prime.ma
@@ -43,11 +43,11 @@ intros.
 apply not_le_to_lt.
 change with smallest_factor (S (fact n)) \le n \to False.intro.
 apply not_divides_S_fact n (smallest_factor(S (fact n))) ? ?.
-apply divides_smallest_factor_n.
-simplify.apply le_S_S.apply le_O_n.
 apply lt_SO_smallest_factor.
 simplify.apply le_S_S.apply le_SO_fact.
 assumption.
+apply divides_smallest_factor_n.
+simplify.apply le_S_S.apply le_O_n.
 qed.
 
 (* mi sembra che il problem sia ex *)