proposition: Lemma ctr_sub_cons bs t r et : ctr_sub (ctr_cons bs t r) et = gtree_sub t bs et + ctr_sub r et.
proof: Proof. by rewrite /ctr_cons; case: gtree_emptyP => //= ->; rewrite gtree_sub_empty. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color chromogram gtree ctree)