mult_num_den@{} q : ' q = (' num q) / ' den q. 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.
Require Import HoTT.HIT.quotient. Require Import Import Frac.