proposition: Lemma Generalized_induction_on_finite_sets : forall P:Ensemble U -> Prop, (forall X:Ensemble U, Finite U X -> (forall Y:Ensemble U, Strict_Included U Y X -> P Y) -> P X) -> forall X:Ensemble U, Finite U X -> P X.
proof: Proof. intros P HP X HX. induction HX as [|X HX IH x Hx] in P, HP. - apply HP; [ auto with sets | ]. now intros Y [->%less_than_empty []]. - enough (forall Y, Included U Y (Add U X x) -> P Y) by auto with sets. revert Hx. apply IH. clear IH X HX. intros Y HY IH' Hx Z HZYx. apply HP; [ apply Finite_downward_closed with (Add _ Y x); auto with sets | ]. intros Z' HZ'Z. pose proof (Strict_inclusion_is_transitive_with_inclusion _ _ _ _ HZ'Z HZYx) as [HZ'Yx Hneq]. case (Included_Add _ _ _ _ HZ'Yx) as [HZ'Y | [Y' [-> HY'Y]]]. + case (classic (Z' = Y)) as [-> | Hneq']. * apply (HP _ HY). intros Y' [HY'Y Hneq']. apply (IH' Y'); auto with sets. * apply (IH' Z'); auto with sets. + apply (IH' Y'); auto with sets. now split; [| intros -> ]. Qed.
imports: Finite_sets Constructive_sets Classical Classical_sets Powerset Powerset_facts Powerset_Classical_facts PeanoNat