dec_recip_0@{} : / 0 = 0. Proof. unfold dec_recip. simpl. unfold Frac.dec_rec;simpl. destruct (decide_rel paths 0 0) as [_|E]. - reflexivity. - destruct E;reflexivity. Qed.
Require Import HoTT.HIT.quotient. Require Import Import Frac.