proposition: Lemma finite_set_induction (s:property): s emptyset -> (forall a b, s a -> s (a +s1 b)) -> forall x, finite_set x -> s x.
proof: Proof. by move => se si x fs; apply: finite_set_induction0 => // a b sa _; apply: si. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)