proposition: Lemma connected_subset A B C : separated A B -> C `<=` A `|` B -> connected C -> C `<=` A \/ C `<=` B.
proof: Proof. move=> AB CAB; have -> : C = (C `&` A) `|` (C `&` B). rewrite predeqE => x; split=> [Cx|[] [] //]. by have [Ax|Bx] := CAB _ Cx; [left|right]. move/connectedP/(_ (fun b => if b then C `&` B else C `&` A)) => /not_and3P[]//. by move/existsNP => [b /set0P/negP/negPn]; case: b => /eqP ->; rewrite !(setU0,set0U); [left|right]; apply: subIset; right. case/not_andP => /eqP/set0P[x []]. - move=> /closureI[cCx cAx] [Cx Bx]; exfalso. by move: AB; rewrite /separated => -[] + _; apply/eqP/set0P; exists x. - move=> [Cx Ax] /closureI[cCx cBx]; exfalso. by move: AB; rewrite /separated => -[] _; apply/eqP/set0P; exists x. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed