proposition: Lemma L02 p: 2 <= p -> 2 * p + 3 <= exp2 p * p.
proof: Proof. induction 1. - compute; auto with arith. - cbn; rewrite PeanoNat.Nat.mul_succ_r; ring_simplify. remember (exp2 m) as X. rewrite (Nat.mul_comm X m)in IHle. rewrite <- (Nat.mul_assoc); lia. Qed.
imports: hydras(Iterates F_alpha E0 Ack AckNotPR) Coq(ArithRing Lia Arith)