proposition: Lemma invR_gt1 x : 0 < x -> (1 < / x) <-> (x < 1).
proof: Proof. move=> x0; split => x1; last by rewrite -invR1; apply ltR_inv. move/ltR_inv : x1; rewrite invRK invR1. by apply => //; exact/invR_gt0. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum) Reals mathcomp(lra) mathcomp(Rstruct)