Require Import Arith. Require Import Omega. Fixpoint power (b:nat)(n:nat){struct n}:nat := match n with 0 => 1 | S p => b * b ^ p end where "n ^ p" := (power n p):nat_scope. Eval compute in (2^6). Lemma L1 : 30 < 2^5. Proof. auto with arith. Qed. Check L1. Check (30 < 2^5). Check Prop. Lemma power_of_plus : forall b n p, b^(n+p) = b^n * b^p. Proof. induction n. simpl. auto with arith. simpl. intros;rewrite <- mult_assoc. rewrite IHn. trivial. Qed. Lemma power_of_plus' : forall b n p, b^(n+p) = b^n * b^p. Restart. induction n;simpl;auto with arith. intro p. rewrite (IHn p); ring. Qed. Print power_of_plus. Print power_of_plus'. Lemma power_positive : forall b n, 0 < b -> 0 < b ^ n. Proof. intros b n H; induction n. simpl; auto with arith. simpl. eapply lt_le_trans. eexact IHn. SearchPattern (_ <= _ * _). generalize (mult_le_compat_r 1 b (b^n)). simpl;auto. omega. Qed. Goal 1 <= 2 ^ 2 ^ 2 ^ 2 ^ 2 ^ 2 . (* 2^65536 chiffres *) apply power_positive. auto. (* Restart. compute. *) Qed. Print Unnamed_thm.