proposition: Lemma CRING_mult3 : forall x y z : R1, Equal (ring_mult x (ring_mult y z)) (ring_mult y (ring_mult x z)).
proof: Proof. intros x y z; try assumption. apply Trans with (ring_mult (ring_mult x y) z); auto with algebra. apply Trans with (ring_mult (ring_mult y x) z); auto with algebra. Qed.
imports: Ring_cat Group_facts Abelian_group_facts