A new theorem

diff --git a/helm/software/matita/library/nat/minimization.ma b/helm/software/matita/library/nat/minimization.ma
index d2cde9b67c56d1b961cfc8832fadbc0e67eaf43a..bc2cc70591a3de6e10d5d1f4604e5958046a32d6 100644 (file)
--- a/helm/software/matita/library/nat/minimization.ma
+++ b/helm/software/matita/library/nat/minimization.ma
@@ -366,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.