proposition: Lemma flip_negate_ne_0 x : -x <> 0 <-> x <> 0.
proof: Proof. split; intros E ?; apply E; apply flip_negate_0;trivial. path_via x. apply involutive. Qed.
imports: HoTT.Classes.theory.groups HoTT.Classes.theory.apartness HoTT.Classes.interfaces.abstract_algebra