proposition: Lemma beth_pow1 m: beth \0c <=c m -> (beth \0c) ^c m = \2c ^c m.
proof: Proof. rewrite beth0 => bm. move/clt_omegaP:NS2 => [ha _]. by apply: (infinite_power1_a ha bm); apply/infinite_c_P2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)