proposition: Lemma size_ctree_pick_rev t t' : ctree_proper h t' -> pred2 0 h.+1 (size (ctree_pick_rev t t')).
proof: Proof. rewrite /ctree_pick_rev; set cs0 := [::]; have: size cs0 + h = h by []. elim: {1 3}h t' cs0 {1}Color0 => [|n IHn] [t1 t2 t3|lf|] et e //=. by rewrite addn0; case: ifP => //= _ ->. rewrite -addSnnS => Het [_ t1ok t2ok t3ok]; set cprr := ctree_pick_rev_rec. case Det1: (cprr _ _ _ t1) => [|e1 et1]; last by rewrite -Det1; apply: IHn. by case Det2: (cprr _ _ _ t2) => [|e2 et2]; last rewrite -Det2; apply: IHn. 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)