proposition: Lemma big_ord_recr n F : \big[*%M/1]_(i < n.+1) F i = (\big[*%M/1]_(i < n) F (widen_ord (leqnSn n) i)) * F ord_max.
proof: Proof. transitivity (\big[*%M/1]_(0 <= i < n.+1) F (inord i)). by rewrite big_mkord; apply: eq_bigr=> i _; rewrite inord_val. rewrite big_nat_recr // big_mkord; congr (_ * F _); last first. by apply: val_inj; rewrite /= inordK. by apply: eq_bigr => [] i _; congr F; apply: ord_inj; rewrite inordK //= leqW. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)