proposition: Lemma oprob_divRnnm n m : (0 < n)%nat -> (0 < m)%nat -> (0 < divRnnm n m < 1)%coqR.
proof: Proof. rewrite /divRnnm. split; first by apply divR_gt0; [rewrite ltR0n | rewrite ltR0n addn_gt0 H orTb]. rewrite ltR_pdivr_mulr ?mul1R ?ltR_nat // ?ltR0n ?addn_gt0 ?H ?orTb //. by rewrite -[X in (X < _)%nat](addn0 n) ltn_add2l. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR realType_ext Reals Lra mathcomp(lra)