proposition: Theorem ratDistance_le : forall r1 r2 d, r1 <= d -> r2 <= d -> (ratDistance r1 r2) <= d.
proof: Proof. intuition. unfold ratDistance, maxRat, minRat. case_eq (bleRat r1 r2); intuition; apply ratSubtract_le; eauto. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms