proposition: Theorem ratMult_distrib : forall r1 r2 r3, r1 * (r2 + r3) == r1 * r2 + r1 * r3.
proof: Proof. rattac. inversion H1; clear H1; subst. inversion H0; clear H0; subst. inversion H; clear H; subst. arithNormalize. f_equal. do 5 arithSimplify. do 5 arithSimplify. Qed.
imports: micromega.Lia List FCF.StdNat Arith Lia Setoid RelationClasses Coq.Classes.Morphisms