proposition: Lemma rec_bag (G : graph2) (x : G) : CK4F G -> x \in @CP (skeleton G) IO -> input != output :> G -> CK4F (bgraph IO x) /\ measure (bgraph IO x) < measure G.
proof: Proof. move => [conn_G K4F_G] cp_x Dio. split. - apply: CK4F_sub => //. exact: connected_bag. - suff: (input \notin @bag G IO x) || (output \notin @bag G IO x). { by case/orP; exact: measure_node. } rewrite -negb_and. apply:contraNN Dio => /andP[]. rewrite !(bag_cp conn_G) // => [/eqP-> /eqP-> //||]; by apply CP_extensive; rewrite !inE eqxx. 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)