proposition: Lemma big_const_ord : forall n x, \big[op/idx]_(i < n) x === iter n (op x) idx.
proof: Proof. move=> n x; have e := big_const. rewrite /in_mem /mem //= in e. by rewrite -> e, card_ord; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops