proposition: Lemma nderS' n (m := (n.+1) *(nder n)): nder (n.+1) = if (odd n) then m.+1 else m.-1.
proof: Proof. rewrite/m; clear;elim:n => //n Hr. rewrite nderS Hr /= mulnDr (mulSn n.+1) addnC; case on: (odd n). by rewrite addSn. by rewrite /= -addSn prednK // muln_gt0 /= nbder_even_gt0 // on. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)