proposition: Lemma Rinv_lt_cancel (x y : R) : 0 < y -> / y < / x -> x < y.
proof: Proof. intro Hy ; move/Rlt_not_le => Hxy. apply Rnot_le_lt ; contradict Hxy. by apply Rinv_le_contravar. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)