proposition: Lemma gtr_split_eq A rk r : @gtr_split A rk GtrNil GtrNil GtrNil GtrNil r = rk (gsplit r Gpush) (gsplit r Gskip) (gsplit r Gpop0) (gsplit r Gpop1).
proof: Proof. rewrite /gsplit; move: GtrNil => rn. move: rn {2 4 6 8 10}rn {3 6 9 12 15}rn {4 8 12 16 20}rn. by elim: r => // bs [t1 t2 t3|lf|] r IHr *; rewrite ?gtr_split_some -IHr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color ctree chromogram gtree)