proposition: Theorem rng_add_reg_l : ∀ a b c, (c + a = c + b)%K → (a = b)%K.
proof: Proof. intros a b c Habc; simpl in Habc; simpl. apply rng_add_reg_r with (c := c). rewrite rng_add_comm; symmetry. rewrite rng_add_comm; symmetry. assumption. Qed.
imports: Utf8 Setoid