proposition: Lemma mult_num_den@{} q : ' q = (' num q) / ' den q.
proof: Proof. apply path. red. simpl. rewrite mult_1_l. unfold Frac.dec_rec. simpl. destruct (decide_rel paths (den q) 0) as [E|E];simpl. - destruct (den_ne_0 q E). - rewrite mult_1_r. reflexivity. Qed.
imports: HoTT.HIT.quotient HoTT.Basics.Trunc HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.dec_fields