proposition: Lemma s_of_Rpos_probA (p q r : Rpos) : [s_of (p / (p + (q + r)))%:pos%:pr, (q / (q + r))%:pos%:pr] = ((p + q) / (p + q + r))%:pos%:pr.
proof: Proof. apply val_inj; rewrite /= s_of_pqE /onem /=. rewrite -!RminusE. rewrite (_ : 1%mcR = 1)// -RmultE. field. by split; exact/eqP/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)