proposition: Lemma ctr_split_eq A rk r : @ctr_split A rk CtrNil CtrNil CtrNil r = rk (csplit r Color1) (csplit r Color2) (csplit r Color3).
proof: Proof. rewrite /csplit; move: CtrNil {2 4 6 8}CtrNil {3 6 9 12}CtrNil. elim: r => [|bs t r IHr] r1 r2 r3 //. by case: t => // *; rewrite ?ctr_split_some; apply: IHr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color chromogram gtree ctree)