proposition: Lemma finite_set_induction0 (s:property): s emptyset -> (forall a b, s a -> ~(inc b a) -> s (a +s1 b)) -> forall x, finite_set x -> s x.
proof: Proof. move=> se si x /card_finite_setP cxN. pose r n := forall x, cardinal x = n -> s x. have r0: r \0c by move => y h; rewrite (card_nonempty h). apply: (Nat_induction r0 _ cxN _ (erefl (cardinal x))) => n nN rn y yp. move: (setU1_succ_card (CS_nat nN) yp) => [u [v [yt nvu cu]]]. by rewrite yt; apply: si=>//; apply: rn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)