From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 6 Jun 2008 10:35:16 +0000 (+0000)
Subject: A new theorem
X-Git-Tag: make_still_working~5074
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7ee82ad8d5f0b78674694826d2a0bb16508b3da4;p=helm.git

A new theorem
---

diff --git a/helm/software/matita/library/nat/minimization.ma b/helm/software/matita/library/nat/minimization.ma
index d2cde9b67..bc2cc7059 100644
--- 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.