proposition: Lemma ratDistance_ge_difference: forall r1 r2 d, ratDistance r1 r2 <= d -> ratSubtract r1 d <= r2.
proof: Proof. intuition. eapply (leRat_ratAdd_same_r d). case_eq (bleRat r1 d); intuition. rewrite ratSubtract_0; trivial. eapply ratAdd_leRat_compat; intuition. eapply rat0_le_all. apply bleRat_total in H0. rewrite ratAdd_comm. rewrite ratSubtract_ratAdd_inverse_2; trivial. eapply ratDistance_le_sum; trivial. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms