proposition: Lemma ssplit_disconnected (G:sgraph) (V : {set G}) : (forall x y, x \in V -> y \notin V -> ~~ x -- y) -> diso (sjoin (induced V) (induced (~: V))) G.
proof: Proof. move => HV. set H := sjoin _ _. have cast x (p : x \notin V) : x \in ~: V. by rewrite inE. pose g (x : G) : H := match (@boolP (x \in V)) with | AltTrue p => inl (Sub x p) | AltFalse p => inr (Sub x (cast x p)) end. pose h (x : H) : G := match x with inl x => val x | inr x => val x end. pose g' := @Bij _ _ g h. apply Diso'' with h g. - move => [x|x]; rewrite /g /h. + case: {-}_ /boolP => px. * congr inl. symmetry. apply/eqP. by rewrite sub_val_eq. * case:notF. apply: contraNT px => _. exact: valP. + case: {-}_ /boolP => px. * case:notF. apply: contraTT px => _. move: (valP x). by rewrite !inE. * congr inr. symmetry. apply/eqP. by rewrite sub_val_eq. - move => x. rewrite /g /h. by case: {-}_ /boolP. - move => x y. by case: x=>[x|x]; case: y=>[y|y] xy. - move => x y xy. rewrite /g. case: {-}_/boolP => px;case: {-}_/boolP => py => //. + apply: contraTT xy => _. exact: HV. + apply: contraTT xy => _. rewrite sg_sym. exact: HV. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)