proposition: Lemma simple_rcons x p : simple (rcons p x) = (x \notin fband p) && simple p.
proof: Proof. by rewrite -cats1 simple_cat andbT /= orbF andbC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)