proposition: Lemma divRposxxyC r q : divRposxxy q r = (Prob.p (divRposxxy r q)).~%:pr.
proof: Proof. apply val_inj => /=; rewrite [in RHS]addRC. rewrite [in RHS]RdivE' onem_div// ?addrK//. by rewrite RplusE RdivE'. exact: Rpos_neq0. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR realType_ext Reals Lra mathcomp(lra)