proposition: Lemma ctree_size_proper h t : ctree_proper h t -> ctree_size t = 0 -> t = CtreeEmpty.
proof: Proof. elim: h t => [|h IHh] [] //= t1 t2 t3 [t_ne t1ok t2ok t3ok] szt_0. by move/eqP: szt_0 t_ne; rewrite !addn_eq0 => /and3P[]; do 3?move/eqP/IHh->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color chromogram coloring cfmap) fourcolor(cfcolor dyck ctree initctree gtree initgtree) fourcolor(gtreerestrict ctreerestrict)