proposition: Lemma dec_recip_correct (x : F) Px : / x = // (x;Px).
proof: Proof. apply (left_cancellation_ne_0 (.*.) x). - apply trivial_apart. trivial. - rewrite dec_recip_inverse, reciperse_alt by (apply trivial_apart;trivial). reflexivity. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.fields HoTT.Classes.theory.apartness HoTT.Classes.theory.rings