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