New version of the library. nth_prime, gcd, log.

[helm.git] / helm / matita / library / nat / exp.ma

diff --git a/helm/matita/library/nat/exp.ma b/helm/matita/library/nat/exp.ma
index 6fcd9da0ec646620f36b8546af0d54f1854dad2c..2f0bfbeaf50b8166fd3f95c9cb6b9c83551dd723 100644 (file)
--- a/helm/matita/library/nat/exp.ma
+++ b/helm/matita/library/nat/exp.ma
@@ -15,6 +15,8 @@
 set "baseuri" "cic:/matita/nat/exp".
 
 include "nat/times.ma". 
+include "nat/orders.ma".
+include "higher_order_defs/functions.ma".
 
 let rec exp n m on m\def 
  match m with 
@@ -43,4 +45,54 @@ intros.
 elim q.simplify.rewrite < times_n_O.simplify.reflexivity.
 simplify.rewrite > H.rewrite < exp_plus_times.
 rewrite < times_n_Sm.reflexivity.
-qed.
\ No newline at end of file
+qed.
+
+theorem lt_O_exp: \forall n,m:nat. O < n \to O < exp n m. 
+intros.elim m.simplify.apply le_n.
+simplify.rewrite > times_n_SO.
+apply le_times.assumption.assumption.
+qed.
+
+theorem lt_m_exp_nm: \forall n,m:nat. (S O) < n \to m < exp n m.
+intros.elim m.simplify.reflexivity.
+simplify.
+apply trans_le ? ((S(S O))*(S n1)).
+simplify.
+rewrite < plus_n_Sm.apply le_S_S.apply le_S_S.
+rewrite < sym_plus.
+apply le_plus_n.
+apply le_times.assumption.assumption.
+qed.
+
+theorem exp_to_eq_O: \forall n,m:nat. (S O) < n 
+\to exp n m = (S O) \to m = O.
+intros.apply antisym_le.apply le_S_S_to_le.
+rewrite < H1.change with m < exp n m.
+apply lt_m_exp_nm.assumption.
+apply le_O_n.
+qed.
+
+theorem injective_exp_r: \forall n:nat. (S O) < n \to 
+injective nat nat (\lambda m:nat. exp n m).
+simplify.intros 4.
+apply nat_elim2 (\lambda x,y.exp n x = exp n y \to x = y).
+intros.apply sym_eq.apply exp_to_eq_O n.assumption.
+rewrite < H1.reflexivity.
+intros.apply exp_to_eq_O n.assumption.assumption.
+intros.apply eq_f.
+apply H1.
+(* esprimere inj_times senza S *)
+cut \forall a,b:nat.O < n \to n*a=n*b \to a=b.
+apply Hcut.simplify. apply le_S_S_to_le. apply le_S. assumption.
+assumption.
+intros 2.
+apply nat_case n.
+intros.apply False_ind.apply not_le_Sn_O O H3.
+intros.apply inj_times_r m1.assumption.
+qed.
+
+variant inj_exp_r: \forall p:nat. (S O) < p \to \forall n,m:nat.
+(exp p n) = (exp p m) \to n = m \def
+injective_exp_r.
+
+