proposition: Lemma insertE_cat p1 p2 : insertE (p1 ++ p2) = insertE p1 ++ insertE p2.
proof: Proof. by elim: p1 => //= x p1 ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)