proposition: Lemma expnat_base_S : forall n k, ((expnat k n) + n * (expnat k (pred n)) <= expnat (S k) n)%nat.
proof: Proof. induction n; intuition. simpl in *. eapply Nat.le_trans. 2:{ eapply Nat.add_le_mono. eapply IHn. eapply Nat.mul_le_mono. eapply Nat.le_refl. eapply IHn. } rewrite Nat.mul_add_distr_l. repeat rewrite Nat.mul_assoc. repeat rewrite Nat.add_assoc. eapply Nat.add_le_mono. rewrite Nat.add_comm. eapply Nat.add_le_mono. rewrite <- (Nat.add_0_r (expnat k n)) at 1. eapply Nat.add_le_mono. lia. intuition. intuition. rewrite (Nat.mul_comm k n). rewrite <- (Nat.mul_assoc n). destruct n; simpl; intuition. Qed.
imports: Arith micromega.Lia Coq.NArith.BinNat