proposition: Lemma pl_comm@{} : forall q r, equiv (pl q r) (pl r q).
proof: Proof. intros q r;unfold equiv;simpl. rewrite (mult_comm (den r)), plus_comm. reflexivity. Qed.
imports: HoTT.HIT.quotient HoTT.Basics.Trunc HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.dec_fields