proposition: Lemma le_big_nat_cond n m n' m' (P P' : {pred nat}) (F : nat -> R) : (n' <= n)%N -> (m <= m')%N -> (forall i, (n <= i < m)%N -> P i -> P' i) -> le (\big[op/x]_(n <= i < m | P i) F i) (\big[op/x]_(n' <= i < m' | P' i) F i).
proof: Proof. move=> len'n lemm' PP'i; rewrite uniq_sub_le_big_cond ?filter_uniq ?iota_uniq//. move=> i; rewrite !mem_filter !mem_index_iota => /and3P[Pi ni im]. by rewrite PP'i ?ni//= (leq_trans _ ni)// (leq_trans im). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)