proposition: Lemma expansion_exists2 a: natp a -> exists k f, expansion_of f b k a.
proof: Proof. move=> aN; exists a. exact:(expansion_exists1 aN aN (cpow_M1lt (CS_nat aN) bp)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)