X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fminimization.ma;h=4c55ea6beb9b37a91e752913a0338786cea24952;hb=7da6488b45e5dfc1b675552a7f19c58a6abbff2b;hp=33a75b67bad55c4ed5fe63693d1dd50c1c44c66a;hpb=1b1224fb776aaccb9935e61db36fed1160317621;p=helm.git

diff --git a/matita/matita/lib/arithmetics/minimization.ma b/matita/matita/lib/arithmetics/minimization.ma
index 33a75b67b..4c55ea6be 100644
--- a/matita/matita/lib/arithmetics/minimization.ma
+++ b/matita/matita/lib/arithmetics/minimization.ma
@@ -122,7 +122,7 @@ qed.
 theorem max_f_g: ∀f,g,n.(∀i. i < n → f i = g i) → 
   max n f = max n g.
 #f #g #n (elim n) //
-#m #Hind #ext normalize >ext >Hind //
+#m #Hind #ext normalize >ext normalize in Hind >Hind //
 #i #ltim @ext /2/
 qed.
 
@@ -190,7 +190,7 @@ n ≤ m  → ∀b.min n b f ≤ min m b f.
   [#n #leSO @False_ind /2/ 
   |#n #m #Hind #leSS #b
    (cases (true_or_false (f b))) #fb 
-    [lapply (true_min …fb) //
+    [lapply (true_min …fb) #H >H >H //
     |>false_min // >false_min // @Hind /2/
     ]
   ]
@@ -298,7 +298,7 @@ min n b g ≤ min n b f.
 qed.
 
 theorem f_min_true : ∀ f.∀n,b.
-(∃i:nat. b ≤ i ∧ i < n ∧ f i = true) → f (min n b f) = true. 
+(∃i:nat. b ≤ i ∧ i < n + b ∧ f i = true) → f (min n b f) = true. 
 #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.