proposition: Lemma le_expnat_2 : forall n, (n <= expnat 2 n)%nat.
proof: Proof. induction n; intuition; simpl in *. rewrite Nat.add_0_r. assert (S n = 1 + n)%nat. lia. rewrite H. eapply Nat.add_le_mono. eapply expnat_2_ge_1. trivial. Qed.
imports: Arith micromega.Lia Coq.NArith.BinNat