proposition: Lemma nderS n : nder (n.+2) = (n.+1) * (nder n.+1 + nder n).
proof: Proof. by []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)