proposition: Lemma nb_surj_n1 n: nb_surj n.+1 1 = 1.
proof: Proof. rewrite /nb_surj /bin_conv_inv big_ord_recr /= big_ord_recr /= big_ord0. rewrite bin0 binn exp1n exp0n //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq choice fintype binomial) mathcomp(bigop ssralg poly ssrint) gaia(ssete7)