proposition: Lemma beth_pow4c m a: limit_ordinal a -> (beth a) <=c m -> (beth a) ^c m = \2c ^c m.
proof: Proof. move => sa sb. have ib := (beth_pr1 (proj31 sa)). exact: (infinite_power1_a (infinite_ge2 ib) sb (cle_inf_inf ib sb)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)