proposition: Lemma injective_preserves_0 : (forall x, f x = 0 -> x = 0) -> IsInjective f.
proof: Proof. intros E1 x y E. apply equal_by_zero_sum. apply E1. rewrite preserves_minus, E. apply plus_negate_r. Qed.
imports: HoTT.Classes.theory.groups HoTT.Classes.theory.apartness HoTT.Classes.interfaces.abstract_algebra