X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Flib%2Farithmetics%2Fminimization.ma;h=55a6ddef8fee864fdf0a7c05984ecefd0f10ef52;hb=aad5588b82d0f2991c336f7ac2f3fadd76768eeb;hp=526539b2440d99a5703dd2d7926b8bd238447aca;hpb=342278d86d2ebb11b046dcc9f44cc5d08cd16352;p=helm.git

diff --git a/matita/matita/lib/arithmetics/minimization.ma b/matita/matita/lib/arithmetics/minimization.ma
index 526539b24..55a6ddef8 100644
--- a/matita/matita/lib/arithmetics/minimization.ma
+++ b/matita/matita/lib/arithmetics/minimization.ma
@@ -184,6 +184,7 @@ theorem false_to_lt_max: ∀f,n,m.O < n →
     ]
   ]
 qed.
+
 (* minimization *)
  
 (* min k b f is the minimun i, b ≤ i < b + k s.t. f i;  
@@ -347,3 +348,9 @@ theorem f_min_true : ∀ f.∀n,b.
 #f #n #b cases(min_to_min_spec f n b (min n b f) (refl …)) //
 #Hall * #x * * #leb #ltx #fx @False_ind @(absurd … fx) >Hall /2/
 qed.
+
+theorem lt_min : ∀ f.∀n,b.
+(∃i:nat. b ≤ i ∧ i < n + b ∧ f i = true) → min n b f < n + b. 
+#f #n #b #H cases H #i * * #lebi #ltin #fi_true  
+@(le_to_lt_to_lt … ltin) @true_to_le_min //
+qed.
\ No newline at end of file