proposition: Lemma big_const_nat : forall m n x, \big[op/idx]_(m <= i < n) x === iter (n - m) (op x) idx.
proof: Proof. by move=> *; rewrite -> big_const_seq; rewrite count_predT size_iota; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops