proposition: Lemma insertE_seqb (b : bool) x : insertE (nseq b x) = nseq b x ++ nseq b (edge x).
proof: Proof. by case: b. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)