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. 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.
Require Import