proposition: Theorem expnat_double_le : forall k n, n >= 2 -> expnat n (S k) >= 2 * expnat n k.
proof: Proof. induction k; intuition; simpl in *. lia. rewrite Nat.add_0_r. rewrite <- Nat.mul_add_distr_l. eapply Nat.mul_le_mono. trivial. rewrite <- Nat.add_0_r at 1. rewrite <- Nat.add_assoc. eapply IHk. trivial. Qed.
imports: Arith micromega.Lia Coq.NArith.BinNat