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. ring. rewrite E. now apply dec_recip_0. Qed.
imports: Coq.setoid_ring.Field Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.vectorspace MathClasses.theory.fields MathClasses.theory.strong_setoids MathClasses.theory.rings