proposition: Lemma neg_respect@{} : forall q r, equiv q r -> equiv (- q) (- r).
proof: Proof. unfold equiv;simpl;intros q r E. rewrite <-2!negate_mult_distr_l. rewrite E;reflexivity. Qed.
imports: HoTT.HIT.quotient HoTT.Basics.Trunc HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.dec_fields