proposition: Lemma gtree_sub_empty bs et : gtree_sub GtreeEmpty bs et = 0.
proof: Proof. by apply: match_count_0 => w; rewrite gtree_mem_empty. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color chromogram)