fact: Fixpoint ctree_union_rotlr tl tr {struct tr} := match tl, tr with | CtreeNode tl1 tl2 tl3, CtreeNode tr1 tr2 tr3 => let cur := ctree_union_rotlr in ctree_cons (cur tl3 tr2) (cur tl1 tr3) (cur tl2 tr1) | CtreeLeaf _, CtreeLeaf _ => ctree_simple_leaf | _, _ => ctree_union (ctree_rotl tl) (ctree_rotr tr) end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color)