proposition: Lemma ratDistance_from_0 : forall r, ratDistance 0 r == r.
proof: Proof. intuition. unfold ratDistance, maxRat, minRat. rewrite rat0_le_all. eapply ratSubtract_0_r. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms