proposition: Lemma pcatA u v x y (p : Path u v) (q : Path v x) (r : Path x y) : pcat (pcat p q) r = pcat p (pcat q r).
proof: Proof. apply/eqP. by rewrite -val_eqE /= catA. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)