proposition: Lemma rat_distance_of_difference : forall r1 r2 r3 r4 d1 d2, r2 <= r1 -> r4 <= r3 -> ratDistance r1 r3 <= d1 -> ratDistance r2 r4 <= d2 -> ratDistance (ratSubtract r1 r2) (ratSubtract r3 r4) <= (d1 + d2).
proof: Proof. intuition. eapply ratDistance_leRat_both. eapply leRat_trans. eapply ratSubtract_leRat. eapply ratSubtract_leRat. eapply ratDistance_le_sum. eauto. eapply ratDistance_ge_difference. rewrite ratDistance_comm. eauto. eapply leRat_refl. eapply leRat_trans. eapply ratSubtract_leRat. rewrite ratAdd_comm. eapply ratSubtract_ratAdd_assoc_le. eapply leRat_refl. rewrite ratSubtract_ratAdd_assoc_le. eapply ratAdd_leRat_compat. intuition. eapply leRat_trans. eapply ratSubtract_leRat. eapply ratSubtract_assoc_le. eapply leRat_refl. rewrite ratAdd_comm. rewrite ratSubtract_ratAdd_assoc_le. rewrite ratSubtract_0. rewrite <- ratAdd_0_r. intuition. intuition. eapply leRat_trans. eapply ratSubtract_leRat. eapply ratSubtract_leRat. eapply ratDistance_le_sum. rewrite ratDistance_comm. eauto. eapply ratDistance_ge_difference. eauto. eapply leRat_refl. eapply leRat_trans. eapply ratSubtract_leRat. rewrite ratAdd_comm. eapply ratSubtract_ratAdd_assoc_le. eapply leRat_refl. rewrite ratSubtract_ratAdd_assoc_le. eapply ratAdd_leRat_compat. intuition. eapply leRat_trans. eapply ratSubtract_leRat. eapply ratSubtract_assoc_le. eapply leRat_refl. rewrite ratAdd_comm. rewrite ratSubtract_ratAdd_assoc_le. rewrite ratSubtract_0. rewrite <- ratAdd_0_r. intuition. intuition. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms