proposition: Theorem cpcolor_proper cp : ctree_proper (cprsize cp).-1 (cpcolor cp).
proof: Proof. rewrite /cpcolor; case Dh: (cprsize cp).-1 => [|h]; last first. have [/= et_ok _] := cpcolor0_correct [::] (rev cp). rewrite /cp_ht0 -/(rev (rev cp)) revK Dh in et_ok. exact: ctree_cons_rot_proper. have [/= et_ok /(_ _)etP] := cpcolor0_correct [:: Color1] (rev cp). move: etP et_ok; rewrite /cp_ht0 -/(rev (rev cp)). case: (cpcolor0 (rev cp)) => // [t1 t2 t3 _| lf]; first by rewrite revK Dh. case=> // [k0 [k0col _] _] _; rewrite revK in k0 k0col. have:= coloring_proper_cpring (cpmap cp) k0col. by rewrite size_proper_cpring size_ring_cpmap -subn_gt0 subn1 Dh. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring cfmap ctree)