proposition: Lemma cpcolor1_cpexpand_rev (cp : cprog) f (et : colseq) : Color0 \notin et -> foldr cpcolor1 f (rev cp) et = foldr cpcolor1 f (rev (cpexpand cp)) et :> ctree.
proof: Proof. have EctE ct: (if ct is CtreeEmpty then CtreeEmpty else ct) = ct by case: ct. elim/last_ind: cp f et => [|cp s IHcp] // f et et'0. rewrite cpexpand_rcons -cats1 !rev_cat !foldr_cat; case Ds: s => [n||||||]. - by rewrite /= -IHcp // mem_rot. - by rewrite /= -IHcp // mem_rotr. - case: et et'0 => [|[] et] //= et'0; rewrite -?IHcp ?ctree_union_Nl ?EctE //; rewrite !cats1 -!rcons_cons !rotr1_rcons //; do !rewrite headI //=. by rewrite ctree_union_sym. - case: et et'0 => [|e1 [|e2 et]] //=; first by rewrite !if_same. rewrite !cats1 -!rcons_cons !rotr1_rcons -!rot1_cons !size_rot /=. have [<- | ] := altP (e1 =P e2). case: e1 => //= et'0; rewrite -?IHcp ?ctree_union_Nl ?EctE //. by rewrite ctree_union_sym. by case: e1 e2 => [] // [] //= _ et'0; rewrite -!IHcp ?ctree_union_Nl ?EctE. - by rewrite /= -!IHcp. - case: et et'0 => [|e1 [|e2 et]] //=. case: ifPn; rewrite // !inE !negb_or -addc_eq0 => e12_nz /and3P[_ _ et'0]. by apply: IHcp; rewrite inE eq_sym (negPf e12_nz). case: et et'0 => [|e1 [|e2 et]] //= et'0; rewrite -!IHcp//. by case: et et'0 => [|e3 et] // /norP[_ /norP[]]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring cfmap ctree)