proposition: Lemma nonpos_dec_recip_compat x : x ≤ 0 → /x ≤ 0.
proof: Proof. intros. apply flip_nonpos_negate. rewrite dec_recip_negate. apply nonneg_dec_recip_compat. now apply flip_nonpos_negate. Qed.
imports: Coq.Relations.Relation_Definitions Coq.setoid_ring.Ring MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders MathClasses.theory.rings MathClasses.theory.dec_fields MathClasses.orders.rings