proposition: Lemma derange_sum n: \sum_(i<n.+1) 'C(n,i) * (derange i) = n`! /\ \sum_(i<n.+1) 'C(n,i) * (derange i.+1) = n * n`!.
proof: Proof. elim:n => [| n [IH1 IH2]]; first by split; rewrite big_ord_recl big_ord0 //. rewrite factS mulSn -IH2 -IH1;split. rewrite (big_ord_recl n) big_ord_recl /= !bin0 mul1n -addnA; congr (_ + _). exact: (sum_bin_rec n (fun i => (derange (i.+1)))). rewrite -big_split big_distrr /= big_ord_recl add0n; apply: eq_bigr => i _. by rewrite - mulnDr mulnA mul_bin_diag derangeS mulnCA mulnA. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)