proposition: Lemma flip_lt_dec_recip x y : 0 < y → y < x → /x < /y.
proof: Proof. intros E1 E2. assert (0 < x) by now transitivity y. apply (strictly_order_reflecting (x *.)). rewrite dec_recip_inverse. apply (strictly_order_reflecting (y *.)). rewrite (commutativity x), associativity, dec_recip_inverse. now ring_simplify. now apply lt_ne_flip. now apply lt_ne_flip. 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