proposition: Lemma RING_dist_r : forall x y z : R, Equal (ring_mult (sgroup_law R x y) z) (sgroup_law R (ring_mult x z) (ring_mult y z)).
proof: Proof. exact (ring_dist_r_prf R). Qed.
imports: Ring_cat Group_facts Abelian_group_facts