proposition: Lemma subset_le_big [I : finType] [A A' P : {pred I}] (F : I -> R) : A \subset A' -> le (\big[op/x]_(i in A | P i) F i) (\big[op/x]_(i in A' | P i) F i).
proof: Proof. move=> AA'; apply: sub_le_big => y /andP[yA yP]; apply/andP; split => //. exact: subsetP yA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)