proposition: Lemma RING_op_mult_r : forall x y : R, Equal (ring_mult x (group_inverse R 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 x (sgroup_law R y (group_inverse R y))); auto with algebra. apply Trans with (ring_mult x (monoid_unit R)); auto with algebra. Qed.
imports: Ring_cat Group_facts Abelian_group_facts