proposition: Lemma exp2_mono_weak : forall n p, n<= p -> exp2 n <= exp2 p.
proof: Proof. intros n p H; elim H. - left. - intros ? ? ?; apply Nat.lt_le_incl, exp2_mono; auto with arith. Qed.
imports: Coq(RelationClasses Relations Arith Max Lia) hydras(Exp2) LibHyps(LibHyps) hydras(MoreLibHyps)