X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Fminimization.ma;h=0abed5ad354319674d89e049ca833f804cdaaeec;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=bc60b50aca084c6514d47c9565cafb94d00a1b4c;hpb=fb94e5a71be508516514dfe50528ccfb3cd2da91;p=helm.git

diff --git a/helm/matita/library/nat/minimization.ma b/helm/matita/library/nat/minimization.ma
index bc60b50ac..0abed5ad3 100644
--- a/helm/matita/library/nat/minimization.ma
+++ b/helm/matita/library/nat/minimization.ma
@@ -85,7 +85,7 @@ apply (le_n_O_elim a H2).intro.simplify.rewrite > H4.
 simplify.assumption.
 simplify.
 apply (bool_ind (\lambda b:bool.
-(f (S n1) = b) \to (f ([\lambda b:bool.nat] match b in bool with
+(f (S n1) = b) \to (f (match b in bool with
 [ true \Rightarrow (S n1)
 | false  \Rightarrow (max n1 f)])) = true)).
 simplify.intro.assumption.
@@ -160,7 +160,7 @@ rewrite > (min_aux_O_f f).rewrite < Hcut.assumption.
 apply (antisym_le a m).assumption.rewrite > (minus_n_O m).assumption.
 simplify.
 apply (bool_ind (\lambda b:bool.
-(f (m-(S n)) = b) \to (f ([\lambda b:bool.nat] match b in bool with
+(f (m-(S n)) = b) \to (f (match b in bool with
 [ true \Rightarrow m-(S n)
 | false  \Rightarrow (min_aux n m f)])) = true)).
 simplify.intro.assumption.
@@ -209,3 +209,14 @@ apply le_n_Sn.
 assumption.
 qed.
 
+theorem le_min_aux_r : \forall f:nat \to bool. 
+\forall n,off:nat. (min_aux off n f) \le n.
+intros.
+elim off.simplify.rewrite < minus_n_O.
+elim (f n).simplify.apply le_n.
+simplify.apply le_n.
+simplify.elim (f (n -(S n1))).
+simplify.apply le_plus_to_minus.
+rewrite < sym_plus.apply le_plus_n.
+simplify.assumption.
+qed.