neg_respect@{} : forall q r, equiv q r -> equiv (- q) (- r). Proof. unfold equiv;simpl;intros q r E. rewrite <-2!negate_mult_distr_l. rewrite E;reflexivity. Qed.
Require Import HoTT.HIT.quotient. Require Import Import Frac.