proposition: Lemma ALGEBRA_mult_lin_right : forall (x y : A) (a : R), Equal (algebra_mult x (module_mult a y)) (module_mult a (algebra_mult x y)).
proof: Proof. intros x y a; try assumption. unfold algebra_mult in |- *. auto with algebra. Qed.
imports: Algebra Ring_util