proposition: Lemma le_big_ord_cond n m (P P' : {pred nat}) (F : nat -> R) : (n <= m)%N -> (forall i : 'I_n, P i -> P' i) -> le (\big[op/x]_(i < n | P i) F i) (\big[op/x]_(i < m | P' i) F i).
proof: Proof. move=> nm PP'; rewrite -!big_mkord le_big_nat_cond//= => i ni. by have := PP' (Ordinal ni). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)