proposition: Lemma Finite_Included_In_dec {X : Type} (U V : Ensemble X) : Included U V -> Finite U -> Finite V -> forall x : X, In V x -> In U x \/ ~ In U x.
proof: Proof. intros HUV HU HV. pose proof (Finite_eqdec V HV) as HVdec. induction HU. { intros ?. right. intros ?. contradiction. } intros x0 Hx0. specialize (HVdec x x0) as [Hxx|Hxx]; auto. { apply HUV. right. constructor. } { left. right. apply Singleton_intro. assumption. } unshelve epose proof (IHHU _ x0 Hx0) as [Hx1|Hx1]. { intros ? ?; apply HUV; left; auto. } - left. left. assumption. - right. intros Hx2. inversion Hx2; subst; clear Hx2; try contradiction. inversion H0; subst; clear H0; contradiction. Qed.
imports: Coq(Classical Lia) ZornsLemma(DecidableDec EnsemblesImplicit Families FiniteImplicit FunctionPropertiesEns Powerset_facts Image InverseImage ReverseMath.AddSubtract)