x : PropHolds (0 < x) -> PropHolds (0 < /x). Proof. intros E. apply (strictly_order_reflecting (x *.)). rewrite dec_recip_inverse by (apply orders.lt_ne_flip;trivial). rewrite mult_0_r. solve_propholds. Qed.
Require Import