proposition: Lemma fset_bounded_coind (T : choiceType) (P : {fset T} -> Type) (U : {fset T}): (forall X, (forall Y, Y `<=` U -> X `<` Y -> P Y) -> P X) -> forall X, X `<=` U -> P X.
proof: Proof. move=> Psuper X XsubU; rewrite -[X](fsetDK XsubU)//. have {XsubU}: (U `\` X) `<=` U by rewrite fsubsetDl. elim: (_ `\` X) => {}X IHX XsubU. apply: Psuper => Y /fsetDK<-; rewrite fproperD2l ?fsubsetDl //. by move=> /IHX; apply; rewrite fsubsetDl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)