proposition: Lemma exp2_mono : mono exp2.
proof: Proof. red. induction 1. simpl. generalize (exp2_positive n). generalize (exp2 n). intros; lia. cbn. generalize IHle, (exp2_positive m). generalize (exp2 n), (exp2 m). intros; lia. Qed.
imports: Coq(ArithRing Lia Arith)