proposition: Lemma hull_add (A B : set T) : hull [set a + b | a in A & b in B] = [set a + b | a in hull A & b in hull B].
proof: Proof. rewrite eqEsubset; split. - have conv : is_convex_set [set a + b | a in hull A & b in hull B]. apply/asboolP=>x y p [ax axA] [bx bxB] <- [ay ayA] [by' byB] <-. rewrite avgr_addD; exists (ax <|p|> ay). by move: (hull_is_convex A)=>/asboolP; apply. exists (bx <|p|> by')=>//. by move: (hull_is_convex B)=>/asboolP; apply. apply (@hull_sub_convex _ _ (CSet.Pack (CSet.Mixin conv))), image2_subset; exact (@subset_hull _ _). - move=>x [a [na [ga [da [gaA ->]]]]] [b [nb [gb [db [gbB ->]]]]] <-. rewrite avgnr_add. exists (na * nb)%nat, (fun i => let (i, j) := split_prod i in ga i + gb j), (fdistmap (unsplit_prod (n:=nb)) da `x db); split=>// y [i _ <-]. by case: split_prod=>ia ib; exists (ga ia); [by apply gaA; exists ia |]; exists (gb ib)=>//; apply gbB; exists ib. 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