proposition: Lemma eq_n_comp e e' : connect e =2 connect e' -> n_comp_mem e =1 n_comp_mem e'.
proof: Proof. move=> eq_e [a]; apply: eq_card => x /=. by rewrite !inE /= /roots /root /= (eq_pick (eq_e x)). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)