proposition: Lemma ratSubtract_ratMult_le : forall r1 r2 r3 r4, r1 <= r2 -> r3 <= r4 -> ratSubtract (r2 * r4) (r1 * r3) == (ratSubtract r2 r1) * r3 + (ratSubtract r4 r3) * r1 + (ratSubtract r2 r1) * (ratSubtract r4 r3).
proof: Proof. intuition. destruct (leRat_difference_exists H). destruct (leRat_difference_exists H0). eapply eqRat_trans. apply ratSubtract_eqRat_compat. eapply eqRat_trans. apply ratMult_eqRat_compat. apply H1. apply H2. eapply eqRat_trans. apply ratMult_distrib_r. eapply eqRat_trans. eapply ratAdd_eqRat_compat. apply ratMult_comm. apply ratMult_comm. apply ratAdd_eqRat_compat. apply ratMult_distrib_r. apply ratMult_distrib_r. apply eqRat_refl. eapply eqRat_trans. eapply ratSubtract_eqRat_compat. apply ratAdd_assoc. apply ratMult_comm. eapply eqRat_trans. apply ratSubtract_ratAdd_inverse. rewrite <- ratAdd_assoc. apply ratAdd_eqRat_compat. rewrite ratAdd_comm. apply ratAdd_eqRat_compat. rewrite ratMult_comm. apply ratMult_eqRat_compat. eapply eqRat_symm. eapply eqRat_trans. eapply ratSubtract_eqRat_compat. apply H1. apply eqRat_refl. apply ratSubtract_ratAdd_inverse. intuition. apply ratMult_eqRat_compat. apply eqRat_symm. eapply eqRat_trans. apply ratSubtract_eqRat_compat. apply H2. apply eqRat_refl. apply ratSubtract_ratAdd_inverse. intuition. rewrite ratMult_comm. apply ratMult_eqRat_compat. apply eqRat_symm. eapply eqRat_trans. apply ratSubtract_eqRat_compat. apply H1. apply eqRat_refl. apply ratSubtract_ratAdd_inverse. apply eqRat_symm. eapply eqRat_trans. apply ratSubtract_eqRat_compat. apply H2. apply eqRat_refl. apply ratSubtract_ratAdd_inverse. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms