proposition: Lemma ctree_rotlr_proper h t : ctree_proper h t -> ctree_proper h (ctree_rotlr t).
proof: Proof. move=> t_ok; rewrite ctree_rotlr_spec. by apply: ctree_union_proper; [apply: ctree_rotl_proper | apply: ctree_rotr_proper]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color)