proposition: Lemma RING_op_mult_l : forall x y : R, Equal (ring_mult (group_inverse R x) y) (group_inverse R (ring_mult x y)).
proof: Proof. intros x y; try assumption. apply Sym. apply GROUP_law_inverse. apply Trans with (ring_mult (sgroup_law R x (group_inverse R x)) y); auto with algebra. apply Trans with (ring_mult (monoid_unit R) y); auto with algebra. Qed.
imports: Ring_cat Group_facts Abelian_group_facts