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

diff --git a/matita/matita/lib/arithmetics/exp.ma b/matita/matita/lib/arithmetics/exp.ma
index 1205044be..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 
@@ -48,8 +49,54 @@ qed.
 
 theorem lt_O_exp: ∀n,m:nat. O < n → O < n^m. 
 #n #m (elim m) normalize // #a #Hind #posn 
-@(le_times 1 ? 1) /2/
-qed.
+@(le_times 1 ? 1) /2/ qed.
+
+(* [applyS monotonic_le_minus_r /2/ 
+
+> (minus_Sn_n ?) 
+[cut (∃x.∃y.∃z.(x - y ≤ x - z) = (1 ≤ n ^a))
+  [@ex_intro
+    [|@ex_intro
+      [|@ex_intro
+        [|     
+@(rewrite_r \Nopf  (S  n \sup a - n \sup a )
+ (\lambda x:\Nopf 
+  .(S  n \sup a - n \sup a \le S  n \sup a -(S ?-?))=(x\le  n \sup a ))
+ (rewrite_r \Nopf  ?
+  (\lambda x:\Nopf 
+   .(S  n \sup a - n \sup a \le x)=(S  n \sup a - n \sup a \le  n \sup a ))
+  ( refl … Type[0]  (S  n \sup a - n \sup a \le  n \sup a ) ) (S ?-(S ?-?))
+  (rewrite_r \Nopf  (?-O) (\lambda x:\Nopf .S ?-(S ?-?)=x)
+   (rewrite_l \Nopf  1 (\lambda x:\Nopf .S ?-x=n ^a -O) (minus_S_S ? O) (S ?-?)
+    (minus_Sn_n ?)) ?
+   (minus_n_O ?))) 1
+ (minus_Sn_n  n \sup a ))  
+         
+@(rewrite_r \Nopf  (S ?-?)
+ (\lambda x:\Nopf 
+  .(S  n \sup a - n \sup a \le S  n \sup a -(S ?-?))=(x\le  n \sup a ))
+ (rewrite_r \Nopf  ?
+  (\lambda x:\Nopf 
+   .(S  n \sup a - n \sup a \le x)=(S  n \sup a - n \sup a \le  n \sup a ))
+  ( refl ??) (S ?-(S ?-?))
+  ?) 1
+ (minus_Sn_n ?))
+  [||
+@(rewrite_r \Nopf  (?-O) (\lambda x:\Nopf .S ?-(S ?-?)=x)
+  ???)
+[|<(minus_Sn_n ?)
+@(rewrite_r \Nopf  (?-O) (\lambda x:\Nopf .S ?-(S ?-?)=x)
+ (rewrite_l \Nopf  1 (\lambda x:\Nopf .S ?-x=?-O) 
+    ? (S ?-?)
+    (minus_Sn_n ?)) ??)
+ 
+@(rewrite_r \Nopf  (?-O) (\lambda x:\Nopf .S ?-(S ?-?)=x)
+   (rewrite_l \Nopf  1 (\lambda x:\Nopf .S ?-x=?-O) (minus_S_S ? O) (S ?-?)
+    (minus_Sn_n ?)) ?
+   (minus_n_O ?)))
+
+applyS monotonic_le_minus_r /2/
+qed. *)
 
 theorem lt_m_exp_nm: ∀n,m:nat. 1 < n → m < n^m.
 #n #m #lt1n (elim m) normalize // 
@@ -67,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 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/
   ]
@@ -136,4 +183,4 @@ qed.
 
   
    
-   
\ No newline at end of file
+