proposition: Remark eqm_gcomp : n_comp glink G = n_comp glink G'.
proof: Proof. have [e n f Eenf Ee En Ef] := eqGG'; apply: eq_n_comp. by apply: eq_connect => x y; rewrite {1}/glink /= Ee En Ef. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) mathcomp(choice fintype path fingraph)