proposition: Lemma big_ord_widen_cond n1 n2 (P : pred nat) (F : nat -> R) : n1 <= n2 -> \big[op/idx]_(i < n1 | P i) F i = \big[op/idx]_(i < n2 | P i && (i < n1)) F i.
proof: Proof. by move/big_nat_widen=> len12; rewrite -big_mkord len12 big_mkord. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)