added a function to reorder the metasenv.

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

diff --git a/helm/matita/library/nat/minimization.ma b/helm/matita/library/nat/minimization.ma
index bb3475150092077bed0f14ff915dcf0fc0b531e8..748399fbcc699f20c308228bc8e600e64fc2a4d5 100644 (file)
--- a/helm/matita/library/nat/minimization.ma
+++ b/helm/matita/library/nat/minimization.ma
@@ -87,7 +87,6 @@ apply bool_ind (\lambda b:bool.
 (f (S n1) = b) \to (f ([\lambda b:bool.nat] match b in bool with
 [ true \Rightarrow (S n1)
 | false  \Rightarrow (max n1 f)])) = true) ? ? ?.
-reflexivity.
 simplify.intro.assumption.
 simplify.intro.apply H.
 elim H1.elim H3.generalize in match H5.
@@ -97,6 +96,7 @@ apply ex_intro nat ? a.
 split.apply le_S_S_to_le.assumption.assumption.
 intros.apply False_ind.apply not_eq_true_false ?.
 rewrite < H2.rewrite < H7.rewrite > H6. reflexivity.
+reflexivity.
 qed.
 
 theorem lt_max_to_false : \forall f:nat \to bool. 
@@ -164,7 +164,6 @@ apply bool_ind (\lambda b:bool.
 (f (m-(S n)) = b) \to (f ([\lambda b:bool.nat] match b in bool with
 [ true \Rightarrow m-(S n)
 | false  \Rightarrow (min_aux n m f)])) = true) ? ? ?.
-reflexivity.
 simplify.intro.assumption.
 simplify.intro.apply H.
 elim H1.elim H3.elim H4.
@@ -176,6 +175,7 @@ assumption.assumption.
 absurd f a = false.rewrite < H8.assumption.
 rewrite > H5.
 apply not_eq_true_false.
+reflexivity.
 qed.
 
 theorem lt_min_aux_to_false : \forall f:nat \to bool. 
@@ -191,8 +191,9 @@ apply lt_to_not_le.rewrite < H6.assumption.
 elim H3.
 elim le_to_or_lt_eq (n -(S n1)) m.
 apply H.apply lt_minus_S_n_to_le_minus_n.assumption.
-rewrite < H6.assumption.assumption.
+rewrite < H6.assumption.
 rewrite < H7.assumption.
+assumption.
 qed.
 
 theorem le_min_aux : \forall f:nat \to bool.