proposition: Lemma finSet_rect (T : choiceType) (P : {fset T} -> Type) : (forall X, (forall Y, Y `<` X -> P Y) -> P X) -> forall X, P X.
proof: Proof. move=> ih X; move: (leqnn #|` X|); move: (X in Y in _ <= Y) => Y. elim: #|` _| X => [|n IHn] {Y} X. rewrite leqn0 cardfs_eq0 => /eqP ->; apply: ih. by move=> Y /fproper_ltn_card. move=> Xleq; apply: ih => Y XsubY; apply: IHn. by rewrite -ltnS (leq_trans _ Xleq) // fproper_ltn_card. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)