proposition: Lemma interior_rev (G : sgraph) (x y : G) (p : Path x y): interior (prev p) = interior p.
proof: Proof. apply/setP => z. by rewrite !inE orbC. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)