proposition: Lemma negate_swap_r : forall x y, x - y = -(y - x).
proof: Proof. intros. rewrite groups.negate_sg_op. rewrite involutive. reflexivity. Qed.
imports: HoTT.Classes.theory.groups HoTT.Classes.theory.apartness HoTT.Classes.interfaces.abstract_algebra