proposition: Lemma injective_ens_compose (f : A -> B) (g : B -> C) : range f U V -> injective_ens f U -> injective_ens g V -> injective_ens (compose g f) U.
proof: Proof. firstorder. Qed.
imports: Coq(ClassicalChoice Description Program.Subset) ZornsLemma(DecidableDec EnsemblesImplicit Families FunctionProperties Image InverseImage Powerset_facts Proj1SigInjective) Coq(RelationClasses)