proposition: Lemma nb_surj_n2 n: nb_surj n.+1 2 = (2 ^n.+1 - 2)%N.
proof: Proof. rewrite /nb_surj /bin_conv_inv ! big_ord_recr /= big_ord0. rewrite exp0n // mulr0 mul0rn !add0r exp1n binn bin1 - signr_odd /= expr0 expr1. rewrite ! mul1r mulr1n mulr1 addrC. have s2: 2 <= (2 ^ n.+1) by rewrite - {1} (expn1 2); apply: leq_pexp2l. by rewrite -{1} (subnK s2) PoszD - addrA addrN addr0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq choice fintype binomial) mathcomp(bigop ssralg poly ssrint) gaia(ssete7)