proposition: Lemma negate_swap_l x y : -x + y = -(x - y).
proof: Proof. rewrite groups.negate_sg_op_distr,involutive. reflexivity. Qed.
imports: HoTT.Classes.theory.groups HoTT.Classes.theory.apartness HoTT.Classes.interfaces.abstract_algebra