ml_assoc@{} q r t : equiv (ml q (ml r t)) (ml (ml q r) t). Proof. red;simpl. rewrite (associativity (num q)), (associativity (den q)). reflexivity. Qed.
Require Import HoTT.HIT.quotient. Require Import Import Frac.