proposition: Theorem Finite_downward_closed_discouraging {X : Type} (U V : Ensemble X) : Finite V -> Included U V -> Finite U <-> (forall x : X, In V x -> In U x \/ ~ In U x) /\ (forall x y : X, In U x -> In U y -> x = y \/ x <> y).
proof: Proof. intros HV HUV. split. - intros HU. split. + apply Finite_Included_In_dec; assumption. + apply Finite_eqdec; assumption. - intros [HU0 HU1]. apply Finite_downward_closed_dec with V; assumption. Qed.
imports: Coq(Classical Lia) ZornsLemma(DecidableDec EnsemblesImplicit Families FiniteImplicit FunctionPropertiesEns Powerset_facts Image InverseImage ReverseMath.AddSubtract)