proposition: Lemma beth_pow2 m a: ordinalp a -> m <=c beth a -> m <> \0c -> (beth (osucc a)) ^c m = beth (osucc a).
proof: Proof. move => oa lmb mz. by rewrite (beth_succ oa) - cpow_pow (cprod_inf lmb (beth_pr1 oa) mz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)