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