proposition: Lemma finsupp_conv_subl a b p : p != 1%:pr -> finsupp b `<=` finsupp (a <|p|> b).
proof: Proof. move=> p1; rewrite convC; apply: finsupp_conv_subr. apply: contra p1 => /eqP/(congr1 val) /= /onem_eq0 p1. exact/eqP/val_inj. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum) mathcomp(finmap) Reals mathcomp(mathcomp_extra) mathcomp(classical_sets boolp cardinality Rstruct reals) mathcomp(ereal topology esum measure probability) ssrR realType_ext Reals_ext ssr_ext ssralg_ext bigop_ext fdist convex