proposition: Lemma ctree_rotlr_spec t : ctree_rotlr t = ctree_union (ctree_rotl t) (ctree_rotr t).
proof: Proof. rewrite /ctree_rotlr; set u := {2 4}t. elim: t u => [t1 IHt1 t2 IHt2 t3 IHt3 | _ _ |] [] //= u1 u2 u3. rewrite {}IHt1 {}IHt2 {}IHt3 [in RHS]ctree_cons_spec. case: ifP => [/ctree_empty_node_eq[] | ne_t]; first by rewrite !ctree_union_Nl. rewrite [in RHS]ctree_cons_spec; case: ifP => // /ctree_empty_node_eq[]. by rewrite !ctree_union_Nr ctree_cons_spec ne_t. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color)