proposition: Lemma n_comp_connect x : n_comp e (connect e x) = 1.
proof: Proof. rewrite -(card1 (root e x)); apply: eq_card => y. apply/andP/eqP => [[/eqP r_y /rootP-> //] | ->] /=. by rewrite inE connect_root roots_root. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)