proposition: Lemma in_tail : z != x -> z \in p -> z \in tail p.
proof: Proof. move => A. by rewrite mem_path nodesE inE (negbTE A). Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)