proposition: Lemma Finite_downward_closed : forall A:Ensemble U, Finite U A -> forall X:Ensemble U, Included U X A -> Finite U X.
proof: Proof. intros A HA. induction HA as [|A HA IHHA]; [ intros X HX | intros X HXAx ]. - rewrite less_than_empty; auto with sets. - destruct (Included_Add _ _ _ _ HXAx) as [|[X' [-> HX'A]]]; auto with sets. Qed.
imports: Finite_sets Constructive_sets Classical Classical_sets Powerset Powerset_facts Powerset_Classical_facts PeanoNat