proposition: Lemma CRING_mult4 : forall a b c d : R1, Equal (ring_mult (ring_mult a b) (ring_mult c d)) (ring_mult (ring_mult a c) (ring_mult b d)).
proof: Proof. intros a b c d; try assumption. apply Trans with (ring_mult a (ring_mult b (ring_mult c d))); auto with algebra. apply Trans with (ring_mult a (ring_mult (ring_mult b c) d)); auto with algebra. apply Trans with (ring_mult a (ring_mult (ring_mult c b) d)); auto with algebra. apply Trans with (ring_mult a (ring_mult c (ring_mult b d))); auto with algebra. Qed.
imports: Ring_cat Group_facts Abelian_group_facts