proposition: Lemma eq_connect e e' : e =2 e' -> connect e =2 connect e'.
proof: Proof. move=> eq_e x y; apply/connectP/connectP=> [] [p e_p ->]; by exists p; rewrite // (eq_path eq_e) in e_p *. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)