proposition: Lemma scaler_addpt : {morph scaler : x y / addpt x y >-> x + y}.
proof: Proof. move=> [p x|] [q y|] /=; rewrite ?(add0r,addr0) //. rewrite avgrE /divRposxxy /= RdivE' onem_div; last exact: Rpos_neq0. rewrite -!RmultE -!RinvE' -!(mulRC (/ _)%coqR) scalerDr !scalerA !mulrA. have ->: (p + q)%coqR * (/ (p + q))%coqR = 1 by apply mulRV; last by apply Rpos_neq0. by rewrite !mul1r (addRC p) addrK. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg fingroup perm matrix) mathcomp(mathcomp_extra boolp classical_sets Rstruct) mathcomp(ssrnum ereal) mathcomp(lra Rstruct reals) Reals ssrR Reals_ext Ranalysis_ext ssr_ext ssralg_ext logb realType_ext fdist