proposition: Lemma ctree_size_partition t t' t'' : ctree_partition t (CtreePair t' t'') -> ctree_size t = ctree_size t' + ctree_size t''.
proof: Proof. have Esz0 t0: (forall et, ctree_mem t0 et = false) -> ctree_size t0 = 0. elim: t0 => [t1 IHt1 t2 IHt2 t3 IHt3 /(_ (_ :: _))nomem | ? _ /(_ [::])|] //=. by rewrite (IHt1 (nomem Color1)) (IHt2 (nomem Color2)) (IHt3 (nomem Color3)). rewrite /=; elim: t => [t1 IHt1 t2 IHt2 t3 IHt3|lf IHlf|] in t' t'' * => Pt. - have:= Pt (_ :: _); case: t' {Pt}(Pt [::]) => // [t1' t2' t3'|]. case: t'' => [t1'' t2'' t3''|lf|] //= _ Pte. rewrite /= (IHt1 _ _ (Pte Color1)) (IHt2 _ _ (Pte Color2)). by rewrite (IHt3 _ _ (Pte Color3)) -!addnA; do !nat_congr. rewrite /= (IHt1 _ CtreeEmpty (Pte Color1)). rewrite (IHt2 _ CtreeEmpty (Pte Color2)). by rewrite (IHt3 _ CtreeEmpty (Pte Color3)) /= !addn0. case: t'' => [t1'' t2'' t3''|lf|] // _ Pte. rewrite /= (IHt1 CtreeEmpty _ (Pte Color1)). rewrite (IHt2 CtreeEmpty _ (Pte Color2)). by rewrite (IHt3 CtreeEmpty _ (Pte Color3)). rewrite /= (IHt1 CtreeEmpty CtreeEmpty (Pte Color1)). rewrite (IHt2 CtreeEmpty CtreeEmpty (Pte Color2)). by rewrite (IHt3 CtreeEmpty CtreeEmpty (Pte Color3)). - case Dt': t' Pt (Pt [::]) => [t1' t2' t3'|lf'|]; last by case: t''. case: t'' => // lf'' Pt _; rewrite -Dt' /= Dt' Esz0 // => et. by case: et (Pt et) => //= e et; rewrite orbF. by move=> Pt _; rewrite /= Esz0 // => et; case: et (Pt et). by move: Pt => /(_ _)/norP/=/all_and2[]; do 2!move=> /(_ _)/negPf/=/Esz0->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color chromogram coloring cfmap) fourcolor(cfcolor dyck ctree initctree gtree initgtree) fourcolor(gtreerestrict ctreerestrict)