proposition: Lemma big_const_nat m n x : \big[op/idx]_(m <= i < n) x = iter (n - m) (op x) idx.
proof: Proof. by rewrite big_const_seq count_predT size_iota. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)