proposition: Lemma aleph_pow_prop1: aleph1 ^c aleph0 = aleph1 -> forall n, natp n -> n <> \0c -> (\aleph n) ^c aleph0 = \aleph n.
proof: Proof. move => H0 n nN nz. move: (cpred_pr nN nz) => [ cp ->]; move: (cpred n) cp; clear n nN nz. apply: Nat_induction; first by rewrite succ_zero. move => n nN. rewrite (succ_of_nat (NS_succ nN)) (succ_of_nat nN) => Hrec. have on :=(OS_nat nN). have osn := (OS_succ on). rewrite (infinite_power2 osn omega_nz) Hrec cprodC cprod_inf //. - by apply: aleph_le_lec; apply /oleSSP; apply: (oleS on). - exact: (CIS_aleph (OS_succ osn)). - exact: (aleph_nz osn). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)