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