proposition: Lemma Finite_downward_closed_dec {X : Type} (V : Ensemble X) (HV : Finite V) (U : Ensemble X) (HUdec : forall x : X, In V x -> In U x \/ ~ In U x) (HUeq : forall x y : X, In U x -> In U y -> x = y \/ x <> y) (HUV: Included U V) : Finite U.
proof: Proof. revert U HUdec HUeq HUV. induction HV; intros U HUdec HUeq HUV. { replace U with (@Empty_set X). { constructor. } apply Extensionality_Ensembles; split; auto. intros ? ?; contradiction. } destruct (HUdec x) as [Hx|Hx]. { right. constructor. } 2: { apply IHHV; auto. - intros y Hy. apply HUdec. left. assumption. - intros y Hy. specialize (HUV y Hy). destruct HUV; auto. destruct H0. contradiction. } replace U with (Add (Subtract U x) x). 2: { symmetry. apply Extensionality_Ensembles. apply Add_Subtract_discouraging. split; auto. } constructor. 2: apply Subtract_not_in. apply IHHV. - intros y Hy. destruct (HUdec y) as [Hy0|Hy0]. { left. assumption. } 2: { right. intros [Hy1 Hy2]. auto. } destruct (HUeq x y Hx Hy0) as [Hxy|Hxy]. + right. subst. apply Subtract_not_in. + left. split; auto. intros Hxy0. apply Singleton_inv in Hxy0. auto. - intros y0 y1 Hy0 Hy1. apply HUeq. + apply Hy0. + apply Hy1. - intros y Hy. destruct Hy as [Hy0 Hy1]. apply HUV in Hy0. destruct Hy0 as [y Hy0|y Hy0]; auto. contradiction. Qed.
imports: Coq(Classical Lia) ZornsLemma(DecidableDec EnsemblesImplicit Families FiniteImplicit FunctionPropertiesEns Powerset_facts Image InverseImage ReverseMath.AddSubtract)