proposition: Lemma walk_of_line e1 e2 (p : @Path line_graph e1 e2) : walk (source e1) (target e2) (nodes p).
proof: Proof. case: p => p pth_p. rewrite nodesE /= eqxx /=. elim: p e1 pth_p => [e1 pth_p|e w IHw e1]. - by rewrite (pathp_nil pth_p) /= eqxx. - by rewrite pathp_cons /edge_rel /= eq_sym => /andP [-> /IHw]. Qed.
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)