X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fmatita%2Flib%2Farithmetics%2Fminimization.ma;fp=matita%2Fmatita%2Flib%2Farithmetics%2Fminimization.ma;h=e558754d04145a8082d244f7f72ee046b723acd6;hb=b4681c749d6e8812fe86d5a9adbf4d4acbc3df06;hp=4c55ea6beb9b37a91e752913a0338786cea24952;hpb=409f569bde067546830df25cd0b1ca898573f66a;p=helm.git

diff --git a/matita/matita/lib/arithmetics/minimization.ma b/matita/matita/lib/arithmetics/minimization.ma
index 4c55ea6be..e558754d0 100644
--- a/matita/matita/lib/arithmetics/minimization.ma
+++ b/matita/matita/lib/arithmetics/minimization.ma
@@ -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 //
     ]
   ]