X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fexp.ma;h=654185c89cb014f498e0bff30a9a0b63b8a4333a;hb=7163f2ff5eb4960162d2fcf135f031ae2a9f8b56;hp=ff0572c82c982a1b01cc82c6f626da0be05e15bd;hpb=b4681c749d6e8812fe86d5a9adbf4d4acbc3df06;p=helm.git

diff --git a/matita/matita/lib/arithmetics/exp.ma b/matita/matita/lib/arithmetics/exp.ma
index ff0572c82..654185c89 100644
--- a/matita/matita/lib/arithmetics/exp.ma
+++ b/matita/matita/lib/arithmetics/exp.ma
@@ -113,7 +113,7 @@ theorem injective_exp_r: ∀b:nat. 1 < b →
 #b #lt1b @nat_elim2 normalize 
   [#n #H @sym_eq @(exp_to_eq_O b n lt1b) //
   |#n #H @False_ind @(absurd (1 < 1) ? (not_le_Sn_n 1))
-   <H in ⊢ (??%) @(lt_to_le_to_lt ? (1*b)) //
+   <H in ⊢ (??%); @(lt_to_le_to_lt ? (1*b)) //
    @le_times // @lt_O_exp /2/
   |#n #m #Hind #H @eq_f @Hind @(injective_times_l … H) /2/
   ]