proposition: Lemma onem_divRxxy (r q : Rpos) : (rpos_coercion r / (rpos_coercion r + q)).~ = q / (q + r).
proof: Proof. rewrite /onem; apply/eqP; rewrite subr_eq. rewrite !RplusE (addrC (r : R)) RdivE' -mulrDl divff//. by rewrite gtR_eqF//; apply: addR_gt0. Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra vector reals normedtype) mathcomp(mathcomp_extra boolp) mathcomp(Rstruct) ssrR realType_ext Reals Lra mathcomp(lra)