proposition: Lemma surjective_ens_char (H : range) : surjective_ens <-> surjective (range_restr H).
proof: Proof. split. - intros H0 [y Hy]. specialize (H0 y Hy) as [x [Hx Hxy]]. subst. exists (exist _ x Hx). apply subset_eq_compat. reflexivity. - intros H0 y Hy. specialize (H0 (exist _ y Hy)) as [[x Hx] Hxy]. exists x; split; auto. cbv in Hxy. apply eq_sig_fst in Hxy. auto. Qed.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(DecidableDec EnsemblesImplicit Families FunctionProperties Image InverseImage Powerset_facts Proj1SigInjective) Coq(RelationClasses)