proposition: Lemma injective_preserves_0 : (∀ x, f x = 0 → x = 0) → Injective f.
proof: Proof. intros E1. split; try apply _. intros x y E. apply equal_by_zero_sum. apply E1. rewrite preserves_minus, E. now apply plus_negate_r. Qed.
imports: Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra