proposition: Lemma big_nat1 n F : \big[*%M/1]_(n <= i < n.+1) F i = F n.
proof: Proof. by rewrite big_ltn // big_geq // mulm1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)