proposition: Lemma flip_lt_recip x y (Py : 0 < y) (ltyx : y < x) : let apy0 := positive_apart_zero y Py in let apx0 := positive_apart_zero x (transitivity Py ltyx) in //(x;apx0) < //(y;apy0).
proof: Proof. assert (0 < x) by (transitivity y;trivial). apply (strictly_order_reflecting (x *.)). rewrite (recip_inverse' x ). rewrite mult_comm. apply (strictly_order_reflecting (y *.)). rewrite mult_assoc, mult_1_r. rewrite (recip_inverse' y), mult_1_l; assumption. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.theory.fields HoTT.Classes.orders.rings