proposition: Lemma ctree_mem_cons_rot t et : ctree_mem (ctree_cons_rot t) et = ctree_mem t (ttail et).
proof: Proof. rewrite /ctree_cons_rot /ttail; case: et => [|e et]. by rewrite /= ctree_mem_seq0 ctree_leaf_cons ctree_mem_0. case: e; try by [rewrite /= !ctree_mem_0]; rewrite ctree_mem_cons {1}/ctree_mem /=; by rewrite ?permt_id -1?ctree_mem_rotl -1?ctree_mem_rotr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color)