proposition: Lemma bigmin_bigcup (A : pred I) (B : I -> {set J}) F : \min_(j in \bigcup_(i in A) B i) F j = \min_(i in A) \min_(j in B i) F j :> 'I_n.+1.
proof: Proof. elim/big_rec2: (RHS); first by rewrite big_set0. by move=> i B0 m iA <-; rewrite bigmin_setU. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple) mathcomp(bigop finset finfun perm fingraph path div)