proposition: Lemma dec_recip_0@{} : / 0 = 0.
proof: Proof. unfold dec_recip. simpl. unfold Frac.dec_rec;simpl. destruct (decide_rel paths 0 0) as [_|E]. - reflexivity. - destruct E;reflexivity. Qed.
imports: HoTT.HIT.quotient HoTT.Basics.Trunc HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.dec_fields