proposition: Lemma beth_pow3 m a: ordinalp a -> beth a <=c m -> (beth (osucc a)) ^c m = \2c ^c m.
proof: Proof. move => oa lmb. have ib:= (beth_pr1 oa). have im:= cle_inf_inf ib lmb. by rewrite (beth_succ oa) - cpow_pow cprodC (cprod_inf lmb im (infinite_nz ib)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)