proposition: Lemma ratDistance_ratMult_le : forall r1 r2 r3 r4 d, (ratDistance r1 r3) <= d -> (ratDistance r2 r4) <= d -> r1 <= 1 -> r2 <= 1 -> r3 <= 1 -> r4 <= 1 -> (ratDistance (r1 * r2) (r3 * r4)) <= (3 / 1) * d.
proof: Proof. intuition. unfold ratDistance, maxRat, minRat in *. case_eq (bleRat r1 r3); intuition; rewrite H5 in H. case_eq (bleRat r2 r4); intuition; rewrite H6 in H0. assert (r1 * r2 <= r3 * r4). apply ratMult_leRat_compat; eauto. rewrite H7. rewrite ratSubtract_ratMult_le; eauto. repeat rewrite ratMult_small_le. rewrite H. rewrite H0. eapply eqRat_impl_leRat. symmetry. eapply ratMult_3_ratAdd. eapply ratSubtract_le. trivial. trivial. trivial. apply bleRat_total in H6. case_eq (bleRat (r1 * r2) (r3 * r4)); intuition. rewrite ratSubtract_leRat. 2:{ eapply ratMult_leRat_compat. eapply leRat_refl. eapply H6. } 2:{ eapply ratMult_leRat_compat. eapply leRat_refl. eapply H6. } rewrite ratSubtract_ratMult_le; eauto. repeat rewrite ratMult_small_le. rewrite H. rewrite H0. eapply eqRat_impl_leRat. symmetry. eapply ratMult_3_ratAdd. eapply ratSubtract_le. trivial. trivial. trivial. apply bleRat_total in H7. eapply leRat_trans. eapply ratSubtract_leRat. eapply ratMult_leRat_compat. eapply H5. eapply leRat_refl. eapply ratMult_leRat_compat. eapply H5. eapply leRat_refl. rewrite ratSubtract_ratMult_le; eauto. repeat rewrite ratMult_small_le. rewrite H. rewrite H0. eapply eqRat_impl_leRat. symmetry. eapply ratMult_3_ratAdd. eapply ratSubtract_le. trivial. trivial. trivial. apply bleRat_total in H5. case_eq (bleRat r2 r4); intuition. rewrite H6 in H0. case_eq (bleRat (r1 * r2) (r3 * r4)); intuition. eapply leRat_trans. eapply ratSubtract_leRat. eapply ratMult_leRat_compat. eapply H5. eapply leRat_refl. eapply ratMult_leRat_compat. eapply H5. eapply leRat_refl. rewrite ratSubtract_ratMult_le; eauto. repeat rewrite ratMult_small_le. rewrite H. rewrite H0. eapply eqRat_impl_leRat. symmetry. eapply ratMult_3_ratAdd. eapply ratSubtract_le. trivial. trivial. trivial. apply bleRat_total in H7. eapply leRat_trans. eapply ratSubtract_leRat. eapply ratMult_leRat_compat. eapply leRat_refl. eapply H6. eapply ratMult_leRat_compat. eapply leRat_refl. eapply H6. rewrite ratSubtract_ratMult_le; eauto. repeat rewrite ratMult_small_le. rewrite H. rewrite H0. eapply eqRat_impl_leRat. symmetry. eapply ratMult_3_ratAdd. eapply ratSubtract_le. trivial. trivial. trivial. rewrite H6 in H0. apply bleRat_total in H6. assert (r3 * r4 <= r1 * r2). eapply ratMult_leRat_compat; eauto. case_eq (bleRat (r1 * r2) (r3 * r4)); intuition. rewrite ratSubtract_0; eauto. eapply rat0_le_all. apply bleRat_total in H8. rewrite ratSubtract_ratMult_le; eauto. repeat rewrite ratMult_small_le. rewrite H. rewrite H0. eapply eqRat_impl_leRat. symmetry. eapply ratMult_3_ratAdd. eapply ratSubtract_le. trivial. trivial. trivial. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms