proposition: Theorem ratDistance_comm : forall r1 r2, eqRat (ratDistance r1 r2) (ratDistance r2 r1).
proof: Proof. intuition. unfold ratDistance, maxRat, minRat. case_eq (bleRat r1 r2); case_eq (bleRat r2 r1); intuition. apply ratSubtract_eqRat_compat; eapply leRat_antisymm; eauto. apply bleRat_total in H. apply bleRat_total in H0. apply ratSubtract_eqRat_compat; eapply leRat_antisymm; eauto. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms