proposition: Lemma prob_invn (m : nat) : (R0 <= / (1 + m)%:R <= R1)%mcR.
proof: Proof. rewrite -(mul1R (/ _)%coqR) (_ : 1%coqR = INR 1) // -/(Rdiv _ _). exact: prob_divRnnm_subproof. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR realType_ext Reals Lra mathcomp(lra)