New version of the library. Several files still do not compile.

[helm.git] / matita / matita / lib / arithmetics / exp.ma

diff --git a/matita/matita/lib/arithmetics/exp.ma b/matita/matita/lib/arithmetics/exp.ma
index 1c7adf69b576a7d3388305a73dd28cf50e083700..1205044be600641cfbbff9af76683e28a2530370 100644 (file)
--- 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.