proposition: Lemma flip_le_dec_recip_l x y : 0 < y → /y ≤ x → /x ≤ y.
proof: Proof. Proof with trivial. intros E1 E2. rewrite <-(dec_recip_involutive y). apply flip_le_dec_recip... now apply pos_dec_recip_compat. 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