proposition: Lemma ctr_decr_some lf1 lf2 lf3 bs t r : let cde := ctr_e_decr bs t in ctr_decr lf1 lf2 lf3 (CtrCons bs t r) = ctr_decr (cde Color1 lf1) (cde Color2 lf2) (cde Color3 lf3) r.
proof: Proof. case: t; by [ move=> t0 t1 t2 t3; rewrite /ctr_e_decr !gtree_sub_node_0 | case: lf1 => //; case: bs => // *; case: lf2; case: lf3 ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color chromogram gtree ctree)