proposition: Lemma n_comp_closure2 x y : n_comp e (closure e (pred2 x y)) = (~~ connect e x y).+1.
proof: Proof. rewrite -(root_connect sym_e) -card2; apply: eq_card => z. apply/idP/idP=> [/andP[/eqP {2}<- /pred0Pn[t /andP[/= ezt exyt]]] |]. by case/pred2P: exyt => <-; rewrite (rootP sym_e ezt) !inE eqxx ?orbT. by case/pred2P=> ->; rewrite !inE roots_root //; apply/existsP; [exists x | exists y]; rewrite !inE eqxx ?orbT sym_e connect_root. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)