proposition: Theorem rng_mul_0_l : ∀ a, (0 * a = 0)%K.
proof: Proof. intros a. assert ((0 * a + a = a)%K) as H. transitivity ((0 * a + 1 * a)%K). rewrite rng_mul_1_l; reflexivity. rewrite <- rng_mul_add_distr_r. rewrite rng_add_0_l, rng_mul_1_l. reflexivity. apply rng_add_reg_r with (c := a). rewrite rng_add_0_l; assumption. Qed.
imports: Utf8 Setoid