proposition: Lemma big_const (I : finType) (A : {pred I}) x : \big[op/idx]_(i in A) x = iter #|A| (op x) idx.
proof: Proof. by have [e <- _ [_ <-]] := big_enumP A; rewrite big_const_seq count_predT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)