fact: Definition pcatS (p1 p2 : pathS) : pathS := let: (existT x p,existT y q) := (p1,p2) in match altP (y.1 =P x.2) with AltTrue E => PathS (pcat p (castL E q)) | AltFalse _ => PathS p end.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)