X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fminimization.ma;h=bc2cc70591a3de6e10d5d1f4604e5958046a32d6;hb=9156537d75378d7a254e93b5a2d036d687cd79ee;hp=22d5030ddb37a12d032f66b489cd87aa7bc01780;hpb=6db38e3d8e4083765f2fce40c7845c9827b9afd0;p=helm.git

diff --git a/helm/software/matita/library/nat/minimization.ma b/helm/software/matita/library/nat/minimization.ma
index 22d5030dd..bc2cc7059 100644
--- a/helm/software/matita/library/nat/minimization.ma
+++ b/helm/software/matita/library/nat/minimization.ma
@@ -12,8 +12,6 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/minimization".
-
 include "nat/minus.ma".
 
 let rec max i f \def
@@ -368,6 +366,22 @@ apply not_eq_true_false.
 reflexivity.
 qed.
 
+theorem f_min_true: \forall f:nat \to bool. \forall m:nat.
+(\exists i. le i m \land f i = true) \to
+f (min m f) = true.
+intros.unfold min.
+apply f_min_aux_true.
+elim H.clear H.elim H1.clear H1.
+apply (ex_intro ? ? a).
+split
+  [split
+    [apply le_O_n
+    |rewrite < plus_n_O.assumption
+    ]
+  |assumption
+  ]
+qed.
+
 theorem lt_min_aux_to_false : \forall f:nat \to bool. 
 \forall n,off,m:nat. n \leq m \to m < (min_aux off n f) \to f m = false.
 intros 3.