proposition: Lemma nb_surj_small n p: nb_surj n (n+p.+1) = 0.
proof: Proof. move: p; elim: n; first by move => p; rewrite add0n nb_surj_0p. by move => n Hrec p; rewrite addSn nb_surj_rec Hrec -addnS Hrec // addr0 mul0rn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq choice fintype binomial) mathcomp(bigop ssralg poly ssrint) gaia(ssete7)