X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fminimization.ma;h=eda9d016618d1031be5b126b65b35ca105b9ee11;hb=7a490593a8c798ac35007ddcc61da3b9153ac619;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..eda9d0166 100644 --- a/matita/matita/lib/arithmetics/minimization.ma +++ b/matita/matita/lib/arithmetics/minimization.ma @@ -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.