proposition: Lemma nb_surj_00 : nb_surj 0 0 = 1.
proof: Proof. rewrite /nb_surj /bin_conv_inv big_ord_recr /= big_ord0. rewrite add0r double_pow_m1 //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq choice fintype binomial) mathcomp(bigop ssralg poly ssrint) gaia(ssete7)