proposition: Lemma sparse_catCA p1 p2 p3 : sparse (p1 ++ p2 ++ p3) = sparse (p2 ++ p1 ++ p3).
proof: Proof. exact: (@simple_catCA (permF G)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap walkup geometry color chromogram)