proposition: Lemma base2_expansion_prop n (F:= the_expansion \2c n) (p := cardinal (domain F)) : natp n -> n <> \0c -> [/\ expansion_of F \2c p n, p <> \0c & Vg F (cpred p) = \1c].
proof: Proof. move => nN nz. move: (the_expansion_pr NS2 clt_12 nN); rewrite -/F -/p; move => [ha hb]. case: (equal_or_not p \0c) => pz. case: nz; move: ha => [hc <-]; apply: csum_trivial; aw. by apply:card_nonempty. split => //; case: hb => // [] [_ hb]. move:ha => [[_ pN _ [pb pc pd]] pe]. suff: inc (cpred p) (domain F) by move => /pd/clt2[]. rewrite pc; apply /(NltP pN); apply: (cpred_lt pN pz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)