pl_comm@{} : forall q r, equiv (pl q r) (pl r q). Proof. intros q r;unfold equiv;simpl. rewrite (mult_comm (den r)), plus_comm. reflexivity. Qed.
Require Import HoTT.HIT.quotient. Require Import Import Frac.