proposition: Lemma ctree_no_decr t n : ~~ ctree_leaf t -> ctree_decr t n = t.
proof: Proof. by case: t n => [t1 t2 t3 | lf |] [|n]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color chromogram gtree ctree)