proposition: Lemma r_of_Rpos_probA (p q r : Rpos) : [r_of (p / (p + (q + r)))%:pos%:pr, (q / (q + r))%:pos%:pr] = (p / (p + q))%:pos%:pr.
proof: Proof. apply/val_inj; rewrite /= r_of_pqE s_of_pqE /onem /=. rewrite -!RminusE -R1E -!RmultE -!RinvE'. field. do 3 (split; first exact/eqP/Rpos_neq0). rewrite (addRC p (q + r)) addRK {4}[in q + r]addRC addRK. rewrite mulRC -mulRBr (addRC _ p) addRA addRK mulR_neq0. 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)