proposition: Lemma F22 n: \sum_(i<n) i `! * i = (n `! ).-1.
proof: Proof. elim: n; first by rewrite big_ord0. move => n Hrec;rewrite big_ord_recr /= Hrec {Hrec}. rewrite factS - {2 3} (prednK (fact_gt0 n)). by rewrite -(add1n n) mulnDl mul1n addSn - pred_Sn mulnC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)