proposition: Lemma invR_le x y : 0 < x -> 0 < y -> / y <= / x -> x <= y.
proof: Proof. move=> x0 y0 H; rewrite -(invRK x) -(invRK y). by apply leR_inv => //; exact/invR_gt0. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)