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