x y : 0 < y -> y ≤ x -> /x ≤ /y. Proof. intros E1 E2. apply (order_reflecting_pos (.*.) x). - apply lt_le_trans with y;trivial. - rewrite dec_recip_inverse. + apply (order_reflecting_pos (.*.) y);trivial. rewrite (commutativity x), simple_associativity, dec_recip_inverse. * rewrite mult_1_l,mult_1_r. trivial. * apply lt_ne_flip;trivial. + apply lt_ne_flip. apply lt_le_trans with y;trivial. Qed.
Require Import