X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fexp.ma;h=c9f2c6984ee6d31aeb1ddc8ab9b96b936b19a9e0;hb=aa5f71baeba0299c0d29be01798f7a1ad13656f9;hp=74a3be71f63d202ed5118663088ac238688d142d;hpb=32d926732ac785220007f1999d8ee868efd12e8c;p=helm.git diff --git a/helm/software/matita/library/nat/exp.ma b/helm/software/matita/library/nat/exp.ma index 74a3be71f..c9f2c6984 100644 --- a/helm/software/matita/library/nat/exp.ma +++ b/helm/software/matita/library/nat/exp.ma @@ -12,8 +12,6 @@ (* *) (**************************************************************************) -set "baseuri" "cic:/matita/nat/exp". - include "nat/div_and_mod.ma". include "nat/lt_arith.ma". @@ -40,6 +38,13 @@ theorem exp_n_SO : \forall n:nat. n = n \sup (S O). intro.simplify.rewrite < times_n_SO.reflexivity. qed. +theorem exp_SO_n : \forall n:nat. S O = (S O) \sup n. +intro.elim n + [reflexivity + |simplify.rewrite < plus_n_O.assumption + ] +qed. + theorem exp_SSO: \forall n. exp n (S(S O)) = n*n. intro.simplify. rewrite < times_n_SO. @@ -146,6 +151,15 @@ apply nat_elim2 ] qed. +theorem lt_exp1: \forall n,m,p:nat. O < p \to n < m \to exp n p < exp m p. +intros. +elim H + [rewrite < exp_n_SO.rewrite < exp_n_SO.assumption + |simplify. + apply lt_times;assumption + ] +qed. + theorem le_exp_to_le: \forall a,n,m. S O < a \to exp a n \le exp a m \to n \le m. intro. @@ -170,6 +184,11 @@ apply nat_elim2;intros ] qed. +theorem le_exp_to_le1 : \forall n,m,p.O < p \to exp n p \leq exp m p \to n \leq m. +intros;apply not_lt_to_le;intro;apply (lt_to_not_le ? ? ? H1); +apply lt_exp1;assumption. +qed. + theorem lt_exp_to_lt: \forall a,n,m. S O < a \to exp a n < exp a m \to n < m. intros. @@ -186,6 +205,23 @@ elim (le_to_or_lt_eq n m) ] ] qed. + +theorem lt_exp_to_lt1: +\forall a,n,m. O < a \to exp n a < exp m a \to n < m. +intros. +elim (le_to_or_lt_eq n m) + [assumption + |apply False_ind. + apply (lt_to_not_eq ? ? H1). + rewrite < H2. + reflexivity + |apply (le_exp_to_le1 ? ? a) + [assumption + |apply lt_to_le. + assumption + ] + ] +qed. theorem times_exp: \forall n,m,p. exp n p * exp m p = exp (n*m) p.