proposition: Lemma ratDistance_le_sum : forall r1 r2 d, ratDistance r1 r2 <= d -> r1 <= r2 + d.
proof: Proof. unfold ratDistance, maxRat, minRat in *. intuition. case_eq (bleRat r1 r2); intuition; rewrite H0 in H. rewrite ratAdd_0_r. eapply ratAdd_leRat_compat. trivial. eapply rat0_le_all. eapply ratSubtract_le_sum. eapply bleRat_total. trivial. trivial. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms