proposition: Lemma exp2_mono1 : forall n p, n <= p -> exp2 n <= exp2 p .
proof: Proof. induction 1; [reflexivity | rewrite exp2S; abstract lia]. Qed.
imports: Coq(Arith Relations Lia) hydras(Hydra_Definitions Hydra_Lemmas Iterates Exp2)