proposition: Lemma minoration : exp2 (exp2 95 * 95) <= N.
proof: Proof. transitivity (exp2 (S M) * S M). - replace (exp2 (exp2 95 * 95)) with ((exp2 (exp2 95 * 95) * 1)). apply Nat.mul_le_mono. + apply exp2_mono1. transitivity M. * apply minoration_2. * right; left. + auto with arith. + apply Nat.mul_1_r. - apply minoration_3. Qed.
imports: Coq(Arith Relations Lia) hydras(Hydra_Definitions Hydra_Lemmas Iterates Exp2)