proposition: Lemma simple_cat p1 p2 : simple (p1 ++ p2) = [&& simple p1, ~~ has (mem (fband p1)) p2 & simple p2].
proof: Proof. rewrite !simple_recI has_fband_sym; elim: p1 => [|x p1 IHp1] //=. by rewrite fband_cat IHp1 !negb_or -!andbA; do !bool_congr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)