proposition: Lemma dec_recip_zero x : / x = 0 <-> x = 0.
proof: Proof. split; intros E. - apply stable. intros Ex. destruct (is_ne_0 1). rewrite <-(dec_recip_inverse x), E by assumption. apply mult_0_r. - rewrite E. apply dec_recip_0. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.theory.fields HoTT.Classes.theory.apartness HoTT.Classes.theory.rings