proposition: Lemma nb_surj_1p p: nb_surj 1 p.+2 = 0.
proof: Proof. set g : ( nat -> int) := fun i => (if i ==1 then 1 else 0)%N. pose f := bin_conv_dir g. have aux: forall i, f i = i. move => i; rewrite /f /g /bin_conv_dir. rewrite big_ord_recl /= mul0rn add0r. case: i; first by rewrite big_ord0. move => i; rewrite big_ord_recl /= bin1 big1 ? addr0. by rewrite - (intz i.+1) pmulrn. by move => [j lji] _ /=; rewrite mul0rn. transitivity (bin_conv_inv f p.+2). congr (_ * _); apply: eq_bigr => i _; rewrite aux //. have H: (forall i, i<=p.+2 -> f i = bin_conv_dir g i) by move => i ip. rewrite - (bin_conv_inv2 H) ?(leqnn p.+2) /g //=. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq choice fintype binomial) mathcomp(bigop ssralg poly ssrint) gaia(ssete7)