proposition: Theorem expnat_ge_1 : forall k n, n > 0 -> 1 <= expnat n k.
proof: Proof. induction k; intuition; simpl in *. rewrite <- Nat.mul_1_r at 1. eapply Nat.mul_le_mono. lia. eauto. Qed.
imports: Arith micromega.Lia Coq.NArith.BinNat