proposition: Lemma big_ord_widen_leq 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=> len12; pose g G i := G (inord i : 'I_(n1.+1)). rewrite -(big_ord_widen_cond (g _ P) (g _ F) len12) {}/g. by apply: eq_big => i *; rewrite inord_val. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)