proposition: Theorem poly_lt_exp : forall c, exists x, forall y, y >= x -> expnat y c < expnat 2 y.
proof: Proof. intuition. exists (expnat 2 (max c 6)). intuition. eapply poly_lt_exp_ge_6. eapply Nat.le_trans. 2:{ eapply H. } eapply Nat.pow_le_mono_r. lia. eapply Nat.le_max_l. eapply Nat.le_trans. 2:{ eapply H. } eapply Nat.pow_le_mono_r. lia. eapply Nat.le_max_r. Qed.
imports: FCF.StdNat FCF.Rat