proposition: Theorem rng_mul_add_distr_r : ∀ x y z, ((x + y) * z = x * z + y * z)%K.
proof: Proof. intros x y z; simpl. rewrite rng_mul_comm. rewrite rng_mul_add_distr_l. rewrite rng_mul_comm. assert (rng_eq (rng_mul z y) (rng_mul y z)) as H. apply rng_mul_comm. rewrite H; reflexivity. Qed.
imports: Utf8 Setoid