proposition: Lemma ctree_max_size_proper h t : ctree_proper h t -> ctree_size t <= 3 ^ h.
proof: Proof. elim: h t => [|h IHh] [t1 t2 t3|lf|] //= [_ t1ok t2ok t3ok]. by rewrite expnS 2!mulSn mul1n !leq_add ?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)