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