proposition: Lemma big_ord_widen_leq : forall n1 n2 (P : pred 'I_(n1.+1)) F, n1 < n2 -> \big[op/idx]_(i < n1.+1 | P i) F i === \big[op/idx]_(i < n2 | P (inord i) && (i <= n1)) F (inord i).
proof: Proof. move=> n1 n2 P F len12; pose g G i := G (inord i : 'I_(n1.+1)). pose e := big_ord_widen_cond (g _ P) (g _ F) len12; unfold g in e; rewrite <- e. by apply: eq_big => i *; rewrite inord_val;try reflexivity. Qed.
imports: ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype finfun paths Setoid Morphisms OperationClasses bigops