proposition: Lemma ctree_cons_rot_proper h t : ctree_proper h t -> ctree_proper h.+1 (ctree_cons_rot t).
proof: Proof. by rewrite /ctree_cons_rot => t_ok; apply: ctree_cons_proper; [| apply: ctree_rotl_proper | apply: ctree_rotr_proper]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color)