proposition: Lemma the_expansion_pr a (z := the_expansion a): natp a -> expansion_normal_of z b (cardinal (domain z)) a.
proof: Proof. pose p z:= expansion_normal_of z b (cardinal (domain z)) a. set E := (sub_fgraphs Nat b). move => aN. have sa: (exists2 x, inc x E & p x). move: (expansion_exists3 aN) => [k [f etc]]. have cdf: k = cardinal (domain f). by move: etc => [[[_ hb _ [_ -> _]] _] _]; rewrite (card_nat hb). move: (expansion_bounded1 (proj1 (proj1 etc))) => xEZ; ex_tac. by rewrite /p - cdf. have sb: singl_val2 (inc^~ E) p. move => f1 f2 _ pf1 _ pf2; exact: (proj1 (expansion_unique1 pf1 pf2)). by move: (select_pr sa sb) => []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)