proposition: Lemma infinite_power1_d m: infinite_c m -> omega0 ^c m = \2c ^c m.
proof: Proof. move => icm. move/clt_omegaP: NS2 => [le2_omega _]. move/infinite_c_P2:(icm) => le1. exact:(infinite_power1_a le2_omega le1 icm). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)