proposition: Lemma infinite_power5_ex: \aleph (omega1 +o omega0) ^c (\aleph \2o) = (\2c ^c (\aleph \2o)) *c ((\aleph omega1) ^c aleph1) *c (\aleph (omega1 +o omega0) ^c aleph0).
proof: Proof. have ha:= OS_aleph OS1. have hb:= OS_omega. have hc:= (CIS_aleph OS2). have hd:= (infinite_nz hc). move: (aleph_le_lec (proj1 olt_02)). rewrite aleph0E /aleph0 -{1 4} (card_card CS_omega) => he. have hi:= (card_card(CS_aleph OS1)). move: (aleph_le_lec (proj1 olt_12)); rewrite - hi => hf. by rewrite (infinite_power5 ha hb hd he) (infinite_power6_0 ha hc hf) hi. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)