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