proposition: Lemma big_ord_widen_cond : forall n1 n2 (P : pred nat) (F : nat -> A), n1 <= n2 -> \big[op/idx]_(i < n1 | P i) F i === \big[op/idx]_(i < n2 | P i && (i < n1)) F i.
proof: Proof. move=> n1 n2 P F len12. rewrite <- big_mkord, (big_nat_widen _ _ _ len12), big_mkord; reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops