proposition: Lemma connected_clink x y : connected G -> exists2 p, path clink x p & y = last x p.
proof: Proof. move=> ccG; apply: connectP; rewrite clink_glink. apply/(rootP glinkC); set rx := root glink x; set ry := root glink y. apply: contraTeq ccG => neq_rxy; rewrite [n_comp _ G](cardD1 ry) (cardD1 rx). by rewrite !inE neq_rxy !(roots_root glinkC). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice fintype path fingraph)