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