pl_neg_l@{} x : equiv (- x + x) 0. Proof. red;simpl. rewrite mult_1_r, mult_0_l. rewrite <-plus_mult_distr_r. rewrite plus_negate_l. apply mult_0_l. Qed.
Require Import HoTT.HIT.quotient. Require Import Import Frac.