proposition: Lemma sub_le_big I [s] (P P' : {pred I}) (F : I -> R) : (forall i, P i -> P' i) -> le (\big[op/x]_(i <- s | P i) F i) (\big[op/x]_(i <- s | P' i) F i).
proof: Proof. move=> PP'; rewrite [X in le _ X](big_AC_mk_monoid opA opC) (bigID P P') /=. under [in X in le _ X]eq_bigl do rewrite (andb_idl (PP' _)). rewrite [X in le X _](big_AC_mk_monoid opA opC). case: (bigop _ _ _) (bigop _ _ _) => [y|] [z|]//=. by rewrite -opA [_ y x]opC opA op_incr. by rewrite opC op_incr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)