proposition: Lemma ctree_rotr_proper h t : ctree_proper h t -> ctree_proper h (ctree_rotr t).
proof: Proof. elim: h t => [|h IHh] [t1 t2 t3|lf|] //= [Hne Ht1 Ht2 Ht3]. by apply: ctree_cons_proper; apply: IHh. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color)