lemma 3.6 subverted

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

diff --git a/helm/software/matita/library/nat/minimization.ma b/helm/software/matita/library/nat/minimization.ma
index 22d5030ddb37a12d032f66b489cd87aa7bc01780..bc2cc70591a3de6e10d5d1f4604e5958046a32d6 100644 (file)
--- 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.