proposition: Theorem rat_distance_of_sum : forall r1 r2 r3 r4, ratDistance (r1 + r2) (r3 + r4) <= (ratDistance r1 r3) + (ratDistance r2 r4).
proof: Proof. intuition. eapply leRat_trans. eapply (ratTriangleInequality _ _ (r3 + r2)). eapply ratAdd_leRat_compat. eapply eqRat_impl_leRat. eapply ratDistance_add_same_r. eapply eqRat_impl_leRat. eapply ratDistance_add_same_l. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms