proposition: Lemma sumt_ctree_pick_rev t t' : sumt (ctree_pick_rev t t') = Color0.
proof: Proof. rewrite /ctree_pick_rev; set cs0 := [::]. have: Color0 +c sumt cs0 = Color0 by []. elim: t' cs0 {1 3}Color0 => // [t1 IHt1 t2 IHt2 t3 IHt3|lf _] et e; last first. by move=> e_et_0 /=; case : ifP. move=> e_et_0 /=; set cprr := ctree_pick_rev_rec. case Det1: (cprr _ _ _ t1) => [|e1 et1]; last first. by rewrite -Det1 IHt1 // [Color1]lock /= -addcA addKc. case Det2: (cprr _ _ _ t2) => [|e2 et2]; last first. by rewrite -Det2 IHt2 // [Color2]lock /= -addcA addKc. by rewrite IHt3 // [Color3]lock /= -addcA addKc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan geometry color chromogram) fourcolor(coloring patch snip sew revsnip kempe) fourcolor(ctree initctree gtree initgtree ctreerestrict) fourcolor(gtreerestrict cfmap cfcolor kempetree)