proposition: Lemma finite_set_induction3 (p: Set -> Set -> Prop) E: (forall a b, inc a E -> inc b E -> exists y, p (doubleton a b) y) -> (forall a b x y, sub a E -> inc b E -> p a x -> p (doubleton x b) y-> p (a +s1 b) y) -> (forall X x, sub X E -> nonempty X -> p X x -> inc x E) -> forall X, finite_set X -> nonempty X -> sub X E -> exists x, p X x.
proof: Proof. move=> p1 p2 p3. apply: finite_set_induction2. move=> a aE; have ae:= (aE _ (set1_1 a)). exact:(p1 a a ae ae). move=> a b p4 nea st. have saE: sub a E by apply: sub_trans st; fprops. have bE: inc b E by apply: st;fprops. have [y py] := (p4 nea saE). have yE:= (p3 _ _ saE nea py). have [z pz] := (p1 _ _ yE bE). exists z; apply: p2 saE bE py pz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)