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