proposition: Lemma expRat_le_half_exists : forall r, ~ 1 <= r -> exists n, expRat r n <= (1/2).
proof: Proof. intuition. destruct r. destruct (le_dec n (pred p)). exists (p)%nat. eapply leRat_trans. eapply expRat_leRat_compat. eapply leRat_terms. eapply l. eapply Nat.le_refl. rewrite expRat_terms. destruct p. destruct x. lia. simpl. destruct (eq_nat_dec x O); subst. rewrite Nat.mul_0_l. rewrite rat_num_0. eapply rat0_le_all. assert (nz (2 * (x * expnat x x))). econstructor. eapply mult_gt_0. lia. eapply mult_gt_0. lia. edestruct (@expnat_nz x x). econstructor. lia. eauto. assert (nz ((expnat (S x) x + x * expnat (S x) x))). econstructor. assert (expnat (S x) x > O). edestruct (expnat_nz). econstructor. eapply g. eauto. remember (x * expnat (S x) x)%nat as a. lia. assert (posnatToNat (pos (2 * (x * expnat x x))) <= posnatToNat (pos (expnat (S x) x + x * expnat (S x) x)))%nat. unfold natToPosnat, posnatToNat. rewrite Nat.mul_assoc. rewrite (Nat.mul_comm 2 x). rewrite <- Nat.mul_assoc. rewrite <- (Nat.add_0_l (x * (2 * expnat x x))). eapply Nat.add_le_mono. intuition. eapply Nat.mul_le_mono. intuition. eapply expnat_base_S_same. lia. eapply leRat_trans. eapply leRat_terms. rewrite <- (Nat.mul_1_l (x * expnat x x)). eapply Nat.le_refl. unfold natToPosnat, posnatToNat. eapply H2. assert (nz (x * expnat x x)). econstructor. eapply mult_gt_0. lia. edestruct (@expnat_nz x x). econstructor. lia. eauto. assert (posnatToNat (pos (2 * (x * expnat x x))) = posnatToNat (posnatMult (pos 2) (pos (x * expnat x x)))). unfold posnatMult, posnatToNat, natToPosnat. trivial. eapply leRat_trans. eapply eqRat_impl_leRat. eapply eqRat_trans. eapply eqRat_terms. eapply eq_refl. eapply H4. eapply ratMult_num_den. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. rewrite <- (ratMult_1_r (1/2)). eapply eqRat_refl. } eapply ratMult_leRat_compat. intuition. eapply eqRat_impl_leRat. eapply num_dem_same_rat1. unfold posnatToNat, natToPosnat. trivial. exfalso. eapply H. eapply rat_ge_1. lia. Unshelve. eapply expnat_nz. destruct p. econstructor. simpl. trivial. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms