proposition: Lemma pcat_idR (x y : G) (p : Path x y) : pcat p (idp y) = p.
proof: Proof. apply: val_inj => /=. by rewrite cats0. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)