proposition: Lemma big_geq : forall m n (P : pred nat) F, m >= n -> \big[op/idx]_(m <= i < n | P i) F i === idx.
proof: Proof. by move=> m n P F ge_m_n; rewrite /index_iota (eqnP ge_m_n); rewrite -> big_nil; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops