proposition: Lemma ratMult_ratSubtract_distrib_r : forall f r1 r2, (ratSubtract r1 r2) * f == ratSubtract (r1 * f) (r2 * f).
proof: Proof. intuition. unfold ratMult, ratSubtract. rattac. inversion H; clear H; subst. arithNormalize. f_equal. do 6 arithSimplify. do 6 arithSimplify. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms