proposition: Theorem ratMult_distrib_r : forall r1 r2 r3, ratMult (ratAdd r2 r3) r1 == ratAdd (ratMult r2 r1) (ratMult r3 r1).
proof: Proof. intuition. rewrite ratMult_comm. rewrite ratMult_distrib. eapply ratAdd_eqRat_compat; eapply ratMult_comm. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms