proposition: Lemma ratDistance_0_r_le : forall r d, r <= d -> ratDistance r 0 <= d.
proof: Proof. intuition. unfold ratDistance, maxRat, minRat. case_eq (bleRat r 0); intuition. rewrite ratSubtract_0; eapply rat0_le_all. apply bleRat_total in H0. rewrite ratSubtract_0_r. trivial. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms