proposition: Lemma ratDistance_add_same_r : forall r1 r2 r3, (ratDistance (r1 + r2) (r3 + r2)) == (ratDistance r1 r3).
proof: Proof. intuition. unfold ratDistance, maxRat, minRat. case_eq (bleRat r1 r3); intuition. assert (r1 + r2 <= r3 + r2). eapply ratAdd_leRat_compat; trivial. eapply leRat_refl. rewrite H0. apply ratSubtract_add_same_r; eauto. apply bleRat_total in H. assert (r3 + r2 <= r1 + r2). eapply ratAdd_leRat_compat; trivial. apply leRat_refl. case_eq (bleRat (r1 + r2) (r3 + r2)); intuition. assert (r1 + r2 == r3 + r2). eapply leRat_antisymm; eauto. repeat rewrite ratSubtract_0. intuition. eapply eqRat_impl_leRat. eapply ratAdd_add_same_r. eauto. eapply eqRat_impl_leRat. eapply eqRat_symm. trivial. apply ratSubtract_add_same_r; eauto. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms