proposition: Lemma beth_pow0 m: m <c beth \0c -> m <> \0c -> (beth \0c) ^c m = beth \0c.
proof: Proof. rewrite beth0; move => /clt_omegaP mN mz. exact:(cpow_inf CIS_omega mN mz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)