proposition: Lemma cdecr_leaf e lf1 lf2 lf3 r : let t := ctree_cons lf1 lf2 lf3 in let et := [:: e] in ctree_proper 1 t -> cdecr e lf1 lf2 lf3 r = ctree_leaf_of (ctree_sub t et - ctr_sub r et).
proof: Proof. move=> /= t_ok. elim: r => [|bs t r IHr] in lf1 lf2 lf3 t_ok *; have{t_ok} Dlf := ctree_proper_leaf_of_val (ctree_proper_sel _ t_ok). - by rewrite /= subn0 ctree_sub_cons; case: e (Dlf e); rewrite ctree_sel_cons. rewrite /cdecr !ctr_decr_some -/(cdecr e) {}IHr /=. congr ctree_leaf_of; move/(_ e): Dlf. rewrite ctree_sel_cons 2!ctree_sub_cons /ctr_e_decr. by case: e => //= ->; rewrite ctree_val_decr !ctree_sub_leaf_of subnDA. do [apply: ctree_cons_proper; move: Dlf]; [move/(_ Color1) | move/(_ Color2) | move/(_ Color3)]; rewrite ctree_sel_cons /ctr_e_decr /= => ->; by rewrite ctree_val_decr; apply: ctree_leaf_of_proper. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq) fourcolor(color chromogram gtree ctree)