proposition: Lemma trace_cpring_eq : et = [:: e1, e2 & et''].
proof: Proof. have:= size_long_cpring x0. rewrite /et (head_proper_cpring coloring_proper_cpring) ltnNge. rewrite -urtrace_trace /= rot1_cons /urtrace last_rcons /= /et''. case Dcp: {1}(drop 2 _) => [|z p]; first by rewrite Dcp /e1 /e2 /= => /eqP <-. by rewrite -map_rcons => /head_long_cpring->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring cfmap ctree)