proposition: Lemma exp2_mono : strict_mono exp2.
proof: Proof. red; induction 1; cbn. - generalize (exp2_positive n); generalize (exp2 n);intros; abstract lia. - generalize IHle, (exp2_positive m); generalize (exp2 n), (exp2 m); intros;abstract lia. Qed.
imports: Coq(RelationClasses Relations Arith Max Lia) hydras(Exp2) LibHyps(LibHyps) hydras(MoreLibHyps)