proposition: Theorem poly_lt_exp_ge_6 : forall c x, x >= (Nat.pow 2 c) -> x >= (Nat.pow 2 6) -> Nat.pow x c < Nat.pow 2 x.
proof: Proof. intuition. specialize (Nat.log2_spec_alt); intuition. destruct (H1 x). eapply Nat.lt_le_trans. 2:{ eapply H. } eapply (expnat_2_ge_1 c). intuition. destruct (eq_nat_dec x0 0). rewrite e in H3. rewrite Nat.add_0_r in *. rewrite H3. rewrite <- Nat.pow_mul_r. eapply Nat.pow_lt_mono_r. lia. rewrite <- H3. assert (c <= Nat.log2 x). eapply (@Nat.pow_le_mono_r_iff 2). lia. rewrite <- H3. trivial. eapply Nat.le_lt_trans. eapply Nat.mul_le_mono. eapply Nat.le_refl. eapply H4. eapply log_square_lt. eapply Nat.le_trans. 2:{ eapply H0. } eapply Nat.pow_le_mono_r. lia. lia. destruct (eq_nat_dec c 0). rewrite e. simpl. eapply Nat.le_lt_trans. assert (1 <= expnat 2 0). trivial. eapply H4. eapply Nat.pow_lt_mono_r. lia. lia. assert (expnat x c < expnat (2 ^ S (Nat.log2 x)) c). eapply Nat.pow_lt_mono_l. lia. eapply Nat.log2_spec. lia. eapply Nat.lt_le_trans. eapply H4. rewrite <- Nat.pow_mul_r. eapply Nat.pow_le_mono_r. lia. assert (c <= S (Nat.log2 x)). eapply (@Nat.pow_le_mono_r_iff 2). lia. eapply Nat.le_trans. eapply H. eapply Nat.lt_le_incl. eapply Nat.log2_spec. lia. eapply Nat.le_trans. eapply Nat.mul_le_mono. eapply Nat.le_refl. eapply H6. eapply S_log_square_lt. eapply Nat.le_trans. 2:{ eapply H0. } eapply Nat.pow_le_mono_r. lia. lia. Qed.
imports: FCF.StdNat FCF.Rat