X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Flib%2Farithmetics%2Fexp.ma;h=5c7500dd976f5f4e9afcc5e0760c5ba156e9fcb5;hb=84b38ac86f1f92b91ae8913cd0dbcb5c3485dc3a;hp=2c3b12d075f864454ee65b7b2881c634df334f89;hpb=ddc80515997a3f56085c6234d4db326141e189aa;p=helm.git

diff --git a/matita/matita/lib/arithmetics/exp.ma b/matita/matita/lib/arithmetics/exp.ma
index 2c3b12d07..5c7500dd9 100644
--- a/matita/matita/lib/arithmetics/exp.ma
+++ b/matita/matita/lib/arithmetics/exp.ma
@@ -10,6 +10,7 @@
       V_______________________________________________________________ *)
 
 include "arithmetics/div_and_mod.ma".
+include "basics/core_notation/exp_2.ma".
 
 let rec exp n m on m ≝ 
  match m with 
@@ -113,7 +114,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 {⊢ (??%)} @(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/
   ]
@@ -182,4 +183,4 @@ qed.
 
   
    
-   
\ No newline at end of file
+