proposition: Lemma connectedU (A B : {set V}) : {in A &, connected} -> {in B &, connected} -> {in A & B, connected} -> {in B & A, connected} -> {in A :|: B &, connected}.
proof: Proof. move=> cA cB cAB cBA z t; rewrite !inE => /orP[zA|zB] /orP[tA|tB]; by[apply: cA|apply: cB|apply: cAB|apply: cBA]. Qed.
imports: HB(structures) mathcomp(all_ssreflect)