proposition: Lemma ffactnSr n m : n ^_ m.+1 = n ^_ m * (n - m).
proof: Proof. elim: n m => [|n IHn] [|m] //=; first by rewrite ffactn1 mul1n. by rewrite !ffactSS IHn mulnA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div fintype tuple finfun bigop prime finset)