proposition: Lemma connect_trans : transitive connect.
proof: Proof. move=> x y z /connectP[p e_p ->] /connectP[q e_q ->]; apply/connectP. by exists (p ++ q); rewrite ?cat_path ?e_p ?last_cat. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(seq path fintype)