proposition: Lemma flip_le_dec_recip x y : 0 < y → y ≤ x → /x ≤ /y.
proof: Proof. Proof with trivial. intros E1 E2. apply (order_reflecting_pos (.*.) x)... now apply lt_le_trans with y. rewrite dec_recip_inverse. apply (order_reflecting_pos (.*.) y)... rewrite (commutativity x), associativity, dec_recip_inverse. now ring_simplify. now apply lt_ne_flip. apply lt_ne_flip. now apply lt_le_trans with y. 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