proposition: Lemma RING_comp : forall x x' y y' : R, Equal x x' -> Equal y y' -> Equal (ring_mult x y) (ring_mult x' y').
proof: Proof. unfold ring_mult in |- *; auto with algebra. Qed.
imports: Ring_cat Group_facts Abelian_group_facts