fact: Fixpoint ctree_proper h t {struct t} : Prop := match t, h with | CtreeEmpty, _ => True | CtreeNode t1 t2 t3, h'.+1 => [/\ ctree_empty_node t = false, ctree_proper h' t1, ctree_proper h' t2 & ctree_proper h' t3] | CtreeLeaf lf, 0 => ctree_proper 0 lf | _, _ => False end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color)