proposition: Lemma del_edge_lift_proof (G : diGraph) (a b x y : G) p : @pathp (del_edge a b) x y p -> @pathp G x y p.
proof: Proof. case: G a b x y p => T e a b x y p. apply: subrel_pathp. exact: subrel_del_edge. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)