proposition: Lemma is_convex_setP (X : set T) : is_convex_set X = is_convex_set_n X.
proof: Proof. apply/idP/idP => H; apply/asboolP. elim => [g d|n IH g d]; first by move: (fdistI0_False d). case: n => [|n] in IH g d * => gX. rewrite {IH} (@Convn_proj _ _ _ _ ord0) //. exact/gX/classical_sets.imageP. by apply/eqP; rewrite fdist1E1 (fdist1I1 d). have [d01|d01] := eqVneq (d ord0) 1%coqR. suff -> : <|>_d g = g ord0 by apply gX; exists ord0. by rewrite (@Convn_proj _ _ _ _ ord0). set D : {fdist 'I_n.+1} := fdist_del d01. pose G (i : 'I_n.+1) : T := g (fdist_del_idx (@ord0 _) i). have /(IH _ D) {}IH : range G `<=` X. move=> x -[i _ <-{x}]; rewrite /G /fdist_del_idx ltn0; apply gX. by exists (lift ord0 i). rewrite ConvnIE //. by move/asboolP : H; apply => //; exact/gX/classical_sets.imageP. move=> x y p xX yX. have [->|p1] := eqVneq p 1%:pr; first by rewrite conv1. set g : 'I_2 -> T := fun i => if i == ord0 then x else y. have gX : range g `<=` X by move=> a -[i _ <-]; rewrite /g; case: ifPn. move/asboolP : H => /(_ _ g (fdistI2 p) gX). rewrite ConvnIE; first by rewrite fdistI2E eqxx. move=> p1'. rewrite {1}/g eqxx (_ : probfdist _ _ = p); last first. by apply val_inj; rewrite /= fdistI2E eqxx. by rewrite (_ : <|>_ _ _ = y) // (_ : (fun _ => _) = (fun=> y)) ?ConvnI1E. 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