proposition: Lemma big_nth : forall x0 r (P : pred I) F, \big[op/idx]_(i <- r | P i) F i === \big[op/idx]_(0 <= i < size r | P (nth x0 r i)) (F (nth x0 r i)).
proof: Proof. move=> x0 r P F; rewrite -{1}(mkseq_nth x0 r) /mkseq. by rewrite -> (big_map (nth x0 r)); rewrite /index_iota subn0; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops