proposition: Lemma finite_set_strong_induction (s : property) : (forall x : Set, finite_set x -> (forall y : Set, ssub y x -> s y) -> s x) -> forall x : Set, finite_set x -> s x.
proof: Proof. move=> IH. suff IH1 : forall n, natp n -> (forall x, cardinal x = n -> s x). move=> x fx. apply: (IH1 (cardinal x)) => //. by apply/card_finite_setP. apply: (@Nat_induction1 (fun n => forall x : Set, cardinal x = n -> s x)). move=> n nn IH1 x ecxn. have fx : finite_set x by apply/card_finite_setP; rewrite ecxn. apply: IH => //. move=> y ssyx; apply: (IH1 (cardinal y)) => //. have /strict_sub_smaller/(_ _ ssyx) := fx. by rewrite ecxn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)