proposition: Lemma expnat_base_S_same : forall n, n > 0 -> (2 * (expnat n n) <= expnat (S n) n)%nat.
proof: Proof. intuition. simpl in *. rewrite Nat.add_0_r. eapply Nat.le_trans. 2:{ eapply expnat_base_S. } destruct n; simpl. lia. intuition. Qed.
imports: Arith micromega.Lia Coq.NArith.BinNat