proposition: Lemma expe_nat n: natp n -> natp (Nbexp n).
proof: Proof. move => h. apply /card_finite_setP. pose Ek k := gfunctions k \3c. have fi: finite_set (Nintc n) by apply: finite_Nintcc. have:finite_set (unionb (Lg (Nintc n) Ek)). apply:finite_union_finite; rewrite /allf;aw;trivial => k ki; rewrite LgV//. have kN:=(Nint_S ki). rewrite /finite_set. have ->: (cardinal (Ek k)) = cardinal (functions k \3c). by rewrite -/(cpow _ _) cpow_pr0. apply/NatP;apply: (NS_pow NS3 kN). suff: sub (expansions_ext_of n) (unionb (Lg (Nintc n) Ek)). apply/ sub_finite_set. move => f fa; apply/setUb_P;aw; move: (expe_bounded2 h fa) => hb. have hc:inc (cardinal (domain f)) (Nintc n) by move /(NintcP h):hb. move: (Zo_hi fa) => [[[qa qb qc [qd qe qf]] _] _]. exists (cardinal (domain f)) => //; rewrite LgV//; apply/gfunctions_P2; split => //. by move => t /(range_gP qd) [x xdf ->]; apply/(NltP NS3); apply: qf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)