proposition: Lemma fact_prod n : n`! = \prod_(1 <= i < n.+1) i.
proof: Proof. elim: n => [|n IHn] //; first by rewrite big_nil. by apply/esym; rewrite factS IHn // !big_add1 big_nat_recr //= mulnC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div fintype tuple finfun bigop prime finset)