proposition: Lemma surjective_ens_compose (f : A -> B) (g : B -> C) : surjective_ens f U V -> surjective_ens g V W -> surjective_ens (compose g f) U W.
proof: Proof. intros Hf Hg z Hz. specialize (Hg z Hz) as [y [Hy Hyz]]. subst. specialize (Hf y Hy) as [x [Hx Hxy]]. subst. exists x; split; auto. Qed.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(DecidableDec EnsemblesImplicit Families FunctionProperties Image InverseImage Powerset_facts Proj1SigInjective) Coq(RelationClasses)