proposition: Lemma mem_hull_setU X Y a0 a1 p : X a0 -> Y a1 -> hull (X `|` Y) (a0 <| p |> a1).
proof: Proof. move=> a0X a1y. exists 2, (fun i => if i == ord0 then a0 else a1), (fdistI2 p); split => /=. by move=> _ [i _ <-] /=; case: ifPn => _; [left | right]. case: Bool.bool_dec => [/eqP|/Bool.eq_true_not_negb H]. rewrite fdistI2E eqxx /= => p1. by rewrite (_ : p = 1%:pr) ?conv1 //; exact/val_inj. congr (_ <| _ |> _); first by apply val_inj; rewrite /= fdistI2E eqxx. case: Bool.bool_dec => // H'. exfalso. move: H'; rewrite fdist_delE fdistD1E (eq_sym (lift _ _)) (negbTE (neq_lift _ _)). rewrite fdistI2E (eq_sym (lift _ _)) (negbTE (neq_lift _ _)) fdistI2E. rewrite eqxx mulrV ?eqxx //. by move: H; rewrite fdistI2E eqxx onem_neq0. 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