proposition: Lemma premaximal_partial_injection: exists x:partial_injection, premaximal partial_injection_ord x.
proof: Proof. apply ZornsLemmaForPreorders. exact partial_injection_preord. exact partial_injection_chain_ub. Qed.
imports: FunctionProperties Relation_Definitions Relation_Definitions_Implicit CSB EnsemblesSpec ClassicalChoice ZornsLemma EnsemblesImplicit ProofIrrelevance FunctionalExtensionality Description