proposition: Lemma bigminU (A B : {set I}) F : \big[min/x]_(i in A :|: B) F i = min (\big[min/x]_(i in A) F i) (\big[min/x]_(i in B) F i).
proof: Proof. apply: le_anti; rewrite le_min bigminUl bigminUr !andbT; apply/bigmin_geP. split=> [|i /[!in_setU]/orP[iA|iB]]; first by rewrite ge_min bigmin_le_id. - by rewrite ge_min bigmin_le_cond. - by rewrite ge_min orbC bigmin_le_cond. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)