proposition: Theorem rng_add_reg_r : ∀ a b c, (a + c = b + c)%K → (a = b)%K.
proof: Proof. intros a b c Habc; simpl in Habc; simpl. apply rng_add_compat_r with (c := (- c)%K) in Habc. do 2 rewrite <- rng_add_assoc in Habc. rewrite rng_add_opp_r in Habc. do 2 rewrite rng_add_0_r in Habc. assumption. Qed.
imports: Utf8 Setoid