proposition: Lemma ratSubtract_ratDistance_le : forall r1 r2, ratSubtract r1 r2 <= ratDistance r1 r2.
proof: Proof. unfold ratDistance, maxRat, minRat in *. intuition. case_eq (bleRat r1 r2); intuition. rewrite ratSubtract_0. eapply rat0_le_all. trivial. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms