proposition: Theorem disjoint_union_lemma f: exists g x, [/\ fgraph g, x = unionb g, (forall i, inc i (domain f) -> (Vg f i) \Eq (Vg g i)) & mutually_disjoint g].
proof: Proof. exists (disjointU_fam f), (disjointU f); split;fprops. move=> i idf; rewrite LgV//; apply:Eq_indexed. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)