proposition: Lemma nbsurj_n2 n: 'Sj(n.+1, 2) = (2 ^n.+1 - 2).
proof: Proof. elim: n => // n Ihn; rewrite nbsurjS Ihn nbsurj_n1 (expnS _ n.+1). rewrite -(subnK (leq_trans(_: 2 <= n.+2) (ltn_expl n.+1 (ltnSn 1)))) //. by rewrite addnK 2!mulnDr (_: 2 * 2 = 2 +2) // addnA addnK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)