proposition: Lemma half_distance_1_le : forall r, ~ 1 <= r -> ~ 1 <= r + (1 / 2) * (ratSubtract 1 r).
proof: Proof. intuition. eapply H. eapply (leRat_ratAdd_same_r 1). rewrite <- (@ratSubtract_sum_1 1 r) at 3; trivial. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. eapply ratAdd_assoc. } repeat rewrite ratMult_2. rewrite ratMult_comm. rewrite (ratMult_comm (2/1)). eapply (@leRat_ratMult_same_r (1/2)). intuition. rewrite ratMult_1_l. rewrite ratMult_eq_rat1. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. symmetry. eapply ratMult_distrib_r. } rewrite ratMult_assoc. rewrite ratMult_eq_rat1. rewrite ratMult_1_r. rewrite ratMult_comm. trivial. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms