proposition: Lemma ratDistance_leRat_both : forall r1 r2 d, ratSubtract r1 r2 <= d -> ratSubtract r2 r1 <= d -> ratDistance r1 r2 <= d.
proof: Proof. intuition. unfold ratDistance, maxRat, minRat. destruct (bleRat r1 r2); trivial. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms