proposition: Lemma connectedP A : connected A <-> forall E : bool -> set T, ~ [/\ forall b, E b !=set0, A = E false `|` E true & separated (E false) (E true)].
proof: Proof. rewrite -propeqE forallNE; apply: notRL; rewrite propeqE; exact: connectedPn. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap generic_quotient) mathcomp(boolp classical_sets functions) mathcomp(cardinality mathcomp_extra fsbigop) reals signed