X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fexp.ma;h=1205044be600641cfbbff9af76683e28a2530370;hb=2343da541bb828ac61079d7811c0fe5613b04fb6;hp=1c7adf69b576a7d3388305a73dd28cf50e083700;hpb=ba7ab956f87c7d483df0dc622f256c6c9d475c7d;p=helm.git

diff --git a/matita/matita/lib/arithmetics/exp.ma b/matita/matita/lib/arithmetics/exp.ma
index 1c7adf69b..1205044be 100644
--- a/matita/matita/lib/arithmetics/exp.ma
+++ b/matita/matita/lib/arithmetics/exp.ma
@@ -75,11 +75,10 @@ qed.
 
 theorem le_exp: ∀n,m,p:nat. O < p →
   n ≤m → p^n ≤ p^m.
-@nat_elim2 
-  [#n #m #ltm #len @lt_O_exp //
-  |#n #m #_ #len @False_ind /2/
-  |#n #m #Hind #p #posp #lenm normalize @le_times //
-   @Hind /2/
+@nat_elim2 #n #m
+  [#ltm #len @lt_O_exp //
+  |#_ #len @False_ind /2/
+  |#Hind #p #posp #lenm normalize @le_times // @Hind /2/
   ]
 qed.