proposition: Lemma aleph0_pr X (x := cardinal X) (c := x +c aleph0): [/\ aleph0 = cardinal Nat, aleph0 = cardinal variables, (x <=c aleph0 -> c = aleph0), aleph0 <=c x -> c = x & [/\ infinite_c c, aleph0 <=c c, cardinal X <=c c & (forall z, aleph0 <=c z -> cardinal X <=c z -> c <=c z ) ]].
proof: Proof. have ha: aleph0 = cardinal Nat by rewrite cardinal_Nat. have hb: aleph0 = cardinal variables by rewrite /variables. have hc:= CIS_aleph0. have ka: x <=c aleph0 -> c = aleph0. move => h; rewrite /c csumC;exact : (csum_inf h hc). have kb: aleph0 <=c x -> c = x. move => h; exact: (csum_inf h (cle_inf_inf hc h)). have hd: infinite_c c. case:(cleT_ee (CS_cardinal X) (proj1 hc)) => h. by rewrite(ka h). rewrite (kb h); exact (cle_inf_inf hc h). move: (csum_Mle0 (cardinal X) (proj1 hc)); rewrite -/c => ua. move: (csum_M0le omega0 (CS_cardinal X)); rewrite -/c => h7. move: (csum_M0le (cardinal X) CS_omega); rewrite csumC -/c => h5. have h6: (forall z, aleph0 <=c z -> cardinal X <=c z -> c <=c z ). move => z za zb; case:(cleT_ee (proj31 za) (proj31 zb)) => h. by rewrite (kb h). by rewrite (ka h). split => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)