fact: Definition ctree_cons t1 t2 t3 := let t := CtreeNode t1 t2 t3 in match t with | CtreeNode CtreeEmpty CtreeEmpty CtreeEmpty => t1 | CtreeNode _ CtreeEmpty CtreeEmpty => t | CtreeNode _ _ CtreeEmpty => t | _ => t end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color)