proposition: Lemma RING_assoc : forall x y z : R, Equal (ring_mult (ring_mult x y) z) (ring_mult x (ring_mult y z)).
proof: Proof. exact (sgroup_assoc_prf (E:=R) (ring_monoid R)). Qed.
imports: Ring_cat Group_facts Abelian_group_facts