proposition: Lemma dec_recip_ne_0_iff x : / x ≠ 0 ↔ x ≠ 0.
proof: Proof. now split; intros E1 E2; destruct E1; apply dec_recip_zero. 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