proposition: Lemma decide_ring_trace (r : seq G) et : {ring_trace r et} + {~ ring_trace r et}.
proof: Proof. pose kpr k p := [pred lc : colseq | (map k p == lc) && (trace (map k r) == et)]. pose ekpr := exists2 k, coloring k & kpr k _ _; pose lc : colseq := [::]. suff: {ekpr [::] lc} + {~ ekpr [::] lc}. case=> [col | no_col]; [left | right]. by have [k colk /eqseqP Det] := col; exists k. by case=> k colk /esym/eqP Det; case: no_col; exists k. move Dn: #|[predC (Nil G)]| => n. elim: n [::] lc Dn => [|n IHn] p lc Dn. have allp x: x \in p := negbFE (card0_eq Dn x). pose kp := nth Color0 lc (index _ p). pose kkp := [pred x | (kp (edge x) == kp x) || (kp (face x) != kp x)]. case kp_ok: (pred0b kkp && kpr kp p lc). case/andP: kp_ok => col_kp Det; left; exists kp => //. by split=> x; [apply negbTE | apply negbNE]; case/norP: (pred0P col_kp x). right=> [[k [kE kF] /andP[/eqP Dlc Det]]]. have Dkp: kp =1 k. by move=> x; rewrite /kp -Dlc (nth_map x) ?nth_index ?index_mem. rewrite /= !(eq_map Dkp) Dlc Det eqxx /= andbT in kp_ok. by case/pred0Pn: kp_ok => x /=; rewrite !Dkp [_ == _]kE [_ == _]kF. have [x p'x | p0] := pickP [predC p]; last by rewrite (eq_card0 p0) in Dn. pose ekprx c := ekpr (x :: p) (c :: lc). have ekprxP c : {ekprx c} + {~ ekprx c}. apply: IHn; rewrite (cardD1 x) [x \in _]p'x in Dn; case: Dn => <-. by apply: eq_card => y; rewrite !inE negb_or. have [cb /= cb_ok | no_cb] := pickP [pred cb | ekprxP (ccons cb.1 cb.2)]. left; move: (ccons _ _) (ekprxP _) cb_ok => c [] // [k col_k] /=. by rewrite eqseq_cons -andbA => /andP[]; exists k. right=> [[k colk kpr_k]]; pose cb := (cbit1 (k x), cbit0 (k x)). case/idP: (no_cb cb) => /=; case: (ekprxP _) => // [[]]; exists k => //=. by rewrite ccons_cbits eqseq_cons eqxx. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap walkup geometry color chromogram)