forall q1 q2, equiv q1 q2 -> equiv (opp q1) (opp q2). Proof. unfold equiv;simpl. intros q1 q2 E. rewrite !(plus_comm (neg _)). symmetry. apply E. Qed.
Require Import HoTT.HIT.quotient Require Import Import ring_quote.Quoting.Instances. Module Import PairT.