proposition: Theorem rng_add_move_0_r : ∀ a b, (a + b = 0)%K ↔ (a = - b)%K.
proof: Proof. intros a b. split; intros H. apply rng_add_compat_r with (c := (- b)%K) in H. rewrite <- rng_add_assoc in H. rewrite rng_add_opp_r in H. rewrite rng_add_0_r, rng_add_0_l in H; assumption. rewrite H. rewrite rng_add_opp_l; reflexivity. Qed.
imports: Utf8 Setoid