proposition: Lemma split_K4_nontrivial (G : graph2) : input != output :> G -> lens G -> ~~ @adjacent _ _ G input output -> CK4F G -> 1 < #|components (@sinterval (skeleton G) input output)|.
proof: Proof. move => A B C [D E]. apply/equivalence_partition_gt1P. - move => x y z _ _ _. exact: (sedge_in_equiv (G := skeleton G)). - set H := sinterval _ _. apply: ssplit_K4_nontrivial (E) (D). + by rewrite /edge_rel/=/sk_rel A. + by case/and3P : B. Qed.
imports: Coq(RelationClasses Morphisms Setoid Lia) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries) GraphTheory(digraph sgraph minor checkpoint cp_minor) GraphTheory(setoid_bigop structures pttdom ptt) GraphTheory(mgraph mgraph2 skeleton bounded)