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