proposition: Lemma induced2_compN_small (G : graph2) (x : G) : input \notin @component_of G x -> output \notin @component_of G x -> #|induced2 (~: @component_of G x)| < #|G|.
proof: Proof. move => X1 X2. rewrite /= card_sub. apply: proper_card. apply/properP; split => //. - exact/subsetP. - exists x => //. rewrite !inE (@in_component_of G) orbF. apply/negP => /orP[] /eqP ?; subst; by rewrite (@in_component_of G) in X1 X2. Qed.
imports: Coq(RelationClasses Morphisms Setoid) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries set_tac) GraphTheory(digraph sgraph treewidth minor checkpoint) GraphTheory(equiv setoid_bigop structures pttdom ptt) GraphTheory(mgraph mgraph2 ptt mgraph2_tw2 skeleton) GraphTheory(bounded extraction_def extraction_iso excluded)