X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fminimization.ma;h=35f177331aee575a167f5910dd5b018fb4fef130;hb=7163f2ff5eb4960162d2fcf135f031ae2a9f8b56;hp=4c55ea6beb9b37a91e752913a0338786cea24952;hpb=31e8729021717072f88d250ef41527da3488289e;p=helm.git

diff --git a/matita/matita/lib/arithmetics/minimization.ma b/matita/matita/lib/arithmetics/minimization.ma
index 4c55ea6be..35f177331 100644
--- a/matita/matita/lib/arithmetics/minimization.ma
+++ b/matita/matita/lib/arithmetics/minimization.ma
@@ -40,7 +40,7 @@ qed.
 
 theorem lt_max_n : ∀f.∀n. O < n → max n f < n.
 #f #n #posn @(lt_O_n_elim ? posn) #m
-normalize (cases (f m)) normalize apply le_S_S //
+normalize (cases (f m)) normalize @le_S_S //
 @le_max_n qed.
 
 theorem le_to_le_max : ∀f.∀n,m.
@@ -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 normalize in Hind >Hind //
+#m #Hind #ext normalize >ext normalize in Hind; >Hind //
 #i #ltim @ext /2/
 qed.
 
@@ -230,8 +230,8 @@ lemma min_exists: ∀f.∀t,m. m < t → f m = true →
   [#b #lebm #ismin #eqtb @False_ind @(absurd … lebm) <eqtb
    @lt_to_not_le //
   |#d #Hind #b #lebm #ismin #eqt cases(le_to_or_lt_eq …lebm)
-    [#ltbm >false_min /2/ @Hind // 
-      [#i #H #H1 @ismin /2/ | >eqt normalize //]
+    [#ltbm >false_min /2/ @Hind //
+      [#i #H #H1 @ismin /2/ | >eqt normalize //] 
     |#eqbm >true_min //
     ]
   ]