proposition: Lemma ctree_mem_rotlr h t et : let preim_t g := ctree_mem t \o permt g in ctree_proper h t -> ctree_mem (ctree_rotlr t) et = preim_t Eperm312 et || preim_t Eperm231 et.
proof: Proof. rewrite ctree_rotlr_spec /= => t_ok. by rewrite -ctree_mem_rotl -ctree_mem_rotr (@ctree_mem_union h) //; [apply: ctree_rotl_proper | apply: ctree_rotr_proper]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color)