proposition: Lemma interior0E p : x != y -> irred p -> interior p = set0 -> exists xy, p = edgep xy.
proof: Proof. move => xNy Ip P0. case: (splitL p xNy) Ip => z [xz] [p'] [E _]. rewrite E irred_edgeL => /andP [xNp Ip']. suff zNy : z = y. { subst. exists xz. by rewrite (irredxx Ip') pcat_idR. } apply: contra_eq P0 => C. apply/set0Pn. exists z. rewrite !inE negb_or C eq_sym E mem_pcat mem_edgep !eqxx //= orbT !andbT. apply: contraNneq xNp => ?. subst z. exact: path_begin. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)