proposition: Lemma bigmaxU (A B : {set I}) F : \big[max/x]_(i in A :|: B) F i = max (\big[max/x]_(i in A) F i) (\big[max/x]_(i in B) F i).
proof: Proof. apply: le_anti; rewrite ge_max bigmaxUl bigmaxUr !andbT; apply/bigmax_leP. split=> [|i /[!in_setU]/orP[iA|iB]]; first by rewrite le_max bigmax_ge_id. - by rewrite le_max le_bigmax_cond. - by rewrite le_max orbC le_bigmax_cond. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)