proposition: Lemma memc0_trace_cpring : (Color0 \in et) = false.
proof: Proof. have [kE kF] := col_k; rewrite -mem_rev -(mem_rot 1) /et -trace_rev. rewrite -map_rev -urtrace_trace urtrace_rot mem_rot. case: (rev _) (cycle_rev_cpring x0) => // x p. rewrite (cycle_path x) [path]lock /urtrace {2}[map]lock /= last_map -!lock. elim: {x p}(x :: p) (last x p) => //= _ p IHp x //= /andP[/eqP<- nxNp]. by rewrite inE IHp // eq_sym addc_eq0 -{1}[x]nodeK (eqcP (kF _)) [_ == _]kE. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring cfmap ctree)