proposition: Lemma big_const : forall (I : finType) (P : pred I) x, \big[op/idx]_(i \in P) x === iter #|P| (op x) idx.
proof: Proof. by move=> I P x; rewrite -> big_const_seq, count_filter, cardE; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops