proposition: Lemma CNFB_card_range x (z := (the_CNFB b x)): ordinalp x -> domain z = cardinal (range z).
proof: Proof. move => ox; move:(the_CNF_p0 bg2 ox) => [[fgz nN pz ax] _]. set f := Lf (Vg z) (domain z) (range z). rewrite - (card_nat nN). suff: bijection f by move/equipotent_aux => /card_eqP. apply: lf_bijective. - by move => t/(inc_V_range fgz). - move => u v udx vdx sv; apply: (CNFB_monomial_inj ox udx vdx). by rewrite/oexp sv. - by move => t /(range_gP fgz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)