proposition: Theorem rng_opp_inj_wd : ∀ a b, (- a = - b)%K ↔ (a = b)%K.
proof: Proof. intros a b; split; intros H. apply rng_add_move_0_r in H. rewrite rng_add_comm in H. apply rng_add_move_0_r in H. rewrite H. apply rng_add_move_0_r. apply rng_add_opp_r. rewrite H; reflexivity. Qed.
imports: Utf8 Setoid