proposition: Lemma connected_n_comp1 (G : sgraph) (x0 : G) : connected [set: G] -> n_comp (--) G = 1.
proof: Proof. move/connectedTE => conG. have E: connect (--) x0 =i G by move => ?; rewrite inE (conG x0). rewrite -(eq_n_comp_r E) n_comp_connect //. exact: sconnect_sym. Qed.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry color coloring walkup combinatorial4ct cfmap) GraphTheory(edone preliminaries bij digraph sgraph) GraphTheory(connectivity minor hmap_ops smerge hcycle arc)