proposition: Lemma ml_assoc@{} q r t : equiv (ml q (ml r t)) (ml (ml q r) t).
proof: Proof. red;simpl. rewrite (associativity (num q)), (associativity (den q)). reflexivity. Qed.
imports: HoTT.HIT.quotient HoTT.Basics.Trunc HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.dec_fields