proposition: Lemma weight_addpt : {morph @weight A : x y / addpt x y >-> x + y}.
proof: Proof. move=> [p x|] [q y|] //=; by rewrite (add0R, addR0). 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