proposition: Theorem ratDistance_eqRat_compat : forall r1 r2 r3 r4, r1 == r3 -> r2 == r4 -> ratDistance r1 r2 == ratDistance r3 r4.
proof: Proof. intuition. unfold ratDistance. eauto using ratSubtract_eqRat_compat, maxRat_eqRat_compat, minRat_eqRat_compat. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms