proposition: Lemma le_big_ord n m [P : {pred nat}] [F : nat -> R] : (n <= m)%N -> le (\big[op/x]_(i < n | P i) F i) (\big[op/x]_(i < m | P i) F i).
proof: Proof. by move=> nm; rewrite (big_ord_widen_cond m)// sub_le_big => //= ? /andP[]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)