proposition: Lemma inverse_map_ens_surjective_ens_range {A B : Type} (f : A -> B) (g : B -> A) U V : surjective_ens f U V -> inverse_map_ens f g U V -> range g V U.
proof: Proof. intros Hf_surj [Hgf Hfg] b Hb. specialize (Hf_surj b Hb) as [a [Ha Hab]]. subst. rewrite Hgf; auto. Qed.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(DecidableDec EnsemblesImplicit Families FunctionProperties Image InverseImage Powerset_facts Proj1SigInjective) Coq(RelationClasses)