proposition: Lemma cpbranch_correct : cp_extcol [::] cpbranch k.
proof: Proof. split; rewrite /cp_ht0 /cp_tr0 /= -/G2 -/et cpbranch_spec. rewrite -size_ring_cpmap -/G2 -(size_map k) -size_trace -/et Det /=. apply: ctree_of_ttail_proper; have [g Eg] := etail_perm et1ok. by move: (congr1 size Eg); rewrite /permt size_map /= => [] [<-]. have eet'0: Color0 \notin etail (behead et). have [g Eg] := etail_perm et1ok. by move: et'0; rewrite Det inE -(memc0_permt g et1) Eg => /norP[]. apply: (iffP (ctree_of_ttail_mem _ eet'0)) => [Det0 | [k0 [_ Det0] Dk]]. exists k => //; split; rewrite // /eptrace {}Det0; congr (etail _). by rewrite /et (head_proper_cpring G2gt1) -urtrace_trace. rewrite {}Det0 /eptrace /et {k0 Dk}(eq_map (Dk : k0 =1 _)). by rewrite (head_proper_cpring G2gt1) -urtrace_trace. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring cfmap ctree)