proposition: Lemma ctr_sub_csplit r e et : ctr_sub (csplit r e) et = (if size et == 0 then 0 else ctr_sub r (e :: et)).
proof: Proof. case Det: {2}et => [|e' et'] /=. rewrite {et}Det; elim: {r e}(csplit r e) => //= [bs t r IHr]. by rewrite IHr addn0; case: t. transitivity (ctr_sub (csplit CtrNil e) et + ctr_sub r (e :: et)); last first. by case: (e). rewrite /csplit /=; move: {2 4}CtrNil {3 6}CtrNil {4 8}CtrNil. elim: r => [|bs t r IHr] r1 r2 r3; first by rewrite /= addn0. have sub0: (forall s s' w, ~~ gtree_mem t [:: s, s' & w]) -> gtree_sub t bs (e :: et) = 0. - rewrite {IHr}Det /gtree_sub; move: (gtree_mem t) => st st0. by case: e e' => [] // [] //=; do 3![rewrite ?match_count_0 //; case: bs => //= bs]. case: t sub0; do [ move=> t0 t1 t2 t3 _; rewrite ctr_split_some {}IHr | by move=> sub0; rewrite /= {}IHr {}sub0 //; case ]. rewrite /= addnA -2!(addnC (ctr_sub r (e :: et))); congr (_ + _); rewrite addnC. have mc_eta := @match_count_eq [eta gtree_mem _] (gtree_mem _) (frefl _). case: e; rewrite //= ctr_sub_cons /gtree_sub /= ?mc_eta //; by case: bs => *; rewrite ?ctr_sub_cons /= ?mc_eta ?addnA ?addn0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color chromogram gtree ctree)