proposition: Lemma flip_negate_0 x : -x = 0 <-> x = 0.
proof: Proof. etransitivity. - apply flip_negate. - rewrite negate_0. apply reflexivity. Qed.
imports: HoTT.Classes.theory.groups HoTT.Classes.theory.apartness HoTT.Classes.interfaces.abstract_algebra