proposition: Theorem rng_mul_opp_l : ∀ a b, ((- a) * b = - (a * b))%K.
proof: Proof. intros a b; simpl. apply rng_add_reg_l with (c := (a * b)%K). rewrite rng_add_opp_r. rewrite <- rng_mul_add_distr_r. rewrite rng_add_opp_r, rng_mul_0_l. reflexivity. Qed.
imports: Utf8 Setoid