proposition: Lemma le_cardinal_ens_transitive : le_cardinal_ens U V -> le_cardinal_ens V W -> le_cardinal_ens U W.
proof: Proof. intros HUV [[H0 H1]|[g [Hg0 Hg1]]]. { left. split; auto. destruct HUV as [[H2 H3]|[f [Hf0 Hf1]]]. { assumption. } intros a Ha. apply (H1 (f a)). apply (Hf0 a Ha). } destruct HUV as [[H0 H1]|[f [Hf0 Hf1]]]. { destruct (classic (inhabited C)). - right. destruct H as [c0]. exists (fun _ => c0). split. + intros a Ha. firstorder. + intros a0 a1 Ha0 Ha1; firstorder. - left. split; auto. } right. exists (compose g f). split. - eapply range_compose; eauto. - eapply injective_ens_compose; eauto. Qed.
imports: Coq(ClassicalChoice Description Lia PeanoNat Program.Subset) ZornsLemma(Cardinals CountableTypes CSB DecidableDec Families Finite_sets FiniteTypes FunctionProperties FunctionPropertiesEns InverseImage Powerset_facts Proj1SigInjective ReverseMath.AddSubtract) Coq(RelationClasses)