proposition: Lemma ctree_val_decr m n : ctree_decr (ctree_leaf_of m) n = ctree_leaf_of (m - n).
proof: Proof. by elim: n m => [|n IHn] [|m] //; apply: IHn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color chromogram gtree ctree)