proposition: Lemma proper_separation_card V1 V2 : proper_separation V1 V2 -> (#|V1| < #|G|)%type * (#|V2| < #|G|)%type.
proof: Proof. by case => [_ [x2 [x1 [HV1 HV2]]]]; rewrite (card_ltnT HV1) (card_ltnT HV2). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph mgraph sgraph set_tac)