x y : -f x = f y -> x = 0 /\ y = 0. Proof. intros E. apply zero_sum, (injective f). rewrite rings.preserves_0, rings.preserves_plus, <-E. apply plus_negate_r. Qed.
Require Import Require Import Import SemiRings.