proposition: Lemma line_of_walk x y w : walk x y w -> ~~ nilp w -> exists e1 e2 (p : @Path line_graph e1 e2), [/\ source e1 = x, target e2 = y & nodes p = w].
proof: Proof. elim: w x => //= e [|e' w] IH x /andP[src_e walk_w] _. - exists e. exists e. exists (@idp line_graph e). rewrite nodesE /idp /= (eqP src_e). split => //. exact/eqP. - case: (IH _ walk_w _) => // e1 [e2] [p] [P1 P2 P3]. have ee1 : @edge_rel line_graph e e1 by apply/eqP; rewrite P1. exists e. exists e2. exists (pcat (edgep ee1) p). rewrite (eqP src_e) P2. split => //. rewrite !nodesE /= in P3 *. case: P3 => ? ?. by subst. Qed.
imports: Coq(Morphisms RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone finite_quotient preliminaries bij) GraphTheory(equiv digraph setoid_bigop structures)