proposition: Lemma le_bigmin2 P F1 F2 : (forall i, P i -> F1 i <= F2 i) -> \big[min/x]_(i | P i) F1 i <= \big[min/x]_(i | P i) F2 i.
proof: Proof. move=> FG; elim/big_ind2 : _ => // a b e f ba fe. rewrite ge_min 2!le_min ba fe /= andbT. move: (le_total a e) => /orP[/(le_trans ba)-> // | /(le_trans fe)->]. by rewrite orbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)