proposition: Theorem expnat_2_monotonic : forall e1 e2, e1 <= e2 -> (expnat 2 e1 <= expnat 2 e2).
proof: Proof. induction e1. intros. simpl. specialize (expnat_2_nz e2). intros. lia. induction e2; intros. lia. simpl. specialize (IHe1 e2). lia. Qed.
imports: ZArith micromega.Lia