proposition: Lemma pl_assoc@{} : forall q r t, equiv (pl q (pl r t)) (pl (pl q r) t).
proof: Proof. intros;unfold equiv;simpl. apply ap011;[|apply symmetry,associativity]. rewrite plus_mult_distr_r. rewrite (plus_mult_distr_r _ _ (den t)). rewrite plus_assoc. apply ap011;[apply ap011|]. - apply associativity. - rewrite <-(associativity (num r)), <-(associativity (num r) (den q)). rewrite (mult_comm (den t)). reflexivity. - rewrite (mult_comm (den q));apply symmetry,associativity. Qed.
imports: HoTT.HIT.quotient HoTT.Basics.Trunc HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.dec_fields