proposition: Lemma convA_set p q (X Y Z : set A) : X :<|p|>: (Y :<|q|>: Z) = (X :<|[r_of p, q]|>: Y) :<|[s_of p, q]|>: Z.
proof: Proof. rewrite eqEsubset; split=> u. - by case=> x Xx; rewrite convA_pt_set=> -[] xy xYxy; exists xy=> //; exists x. - by case=> xy -[] x Xx xYxy; exists x=> //; rewrite convA_pt_set; exists xy. Qed.
imports: HB(structures) Reals mathcomp(all_ssreflect ssralg ssrnum) mathcomp(mathcomp_extra boolp classical_sets Rstruct reals) mathcomp(finmap) Reals_ext realType_ext classical_sets_ext ssrR fdist fsdist convex