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