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