proposition: Lemma cpbranch_spec et : cpbranch et = ctree_of_ttail (etail (behead et)).
proof: Proof. case: et => [|e0 [|e1 et]] //= {e0}. rewrite /etail /etrace_perm /even_trace /ttail /proper_trace /=. case: ifP => //= _; move/edge_rot: e1 => g; elim: et => //= e et IHet. case/g: e; by [ rewrite -IHet; case: ifP | congr (ctree_cons2 _); elim: et {IHet} => //= [[] et <-]]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring cfmap ctree)