proposition: Lemma expe_bounded2 n f: natp n -> inc f (expansions_ext_of n) -> cardinal (domain f) <=c n.
proof: Proof. move => nN /Zo_hi. rewrite / expansion_ext_of_a; set k:= (cardinal (domain f)); move => ha. move:(ha) => [[e1 e2] _]. move:e1 => [pa pb pc [pd pe pf]]. case: (equal_or_not k \0c) => knz; first by rewrite knz; exact(cle0n nN). move: ha; move:(cpred_pr pb knz) => [sa ->]. move/(expe_bounded1 sa) => hb. by move:(clt_leT (cantor (CS_nat sa)) hb); move/(cleSltP sa). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)