proposition: Lemma eq_cardinal_ens_trans {A B C : Type} (U : Ensemble A) (V : Ensemble B) (W : Ensemble C) : eq_cardinal_ens U V -> eq_cardinal_ens V W -> eq_cardinal_ens U W.
proof: Proof. intros [[H0 H1]|[f [Hf0 Hf1]]]. { intros [[H2 H3]|[g [Hg0 Hg1]]]. { left. split; auto. } destruct (classic (inhabited C)). 2: now left; split; auto. right. destruct H as [c]. exists (fun _ => c); split; [|split]. - intros x Hx. specialize (H1 x Hx); contradiction. - intros ? ? Hx. specialize (H1 _ Hx); contradiction. - intros z Hz. destruct Hg1 as [Hg1 Hg2]. specialize (Hg2 z Hz) as [b Hb]. contradiction. } intros [[H0 H1]|[g [Hg0 Hg1]]]. { left. split; auto. intros a Ha. apply (H1 (f a)). apply Hf0. assumption. } right. exists (compose g f). split. - eapply range_compose; eauto. - eapply bijective_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)