proposition: Lemma uniq_ctrenum cp : config_prog cp -> uniq (insertE (cat (cpring (cpmap cp)) (ctrenum cp))).
proof: Proof. elim: cp => //=; case=> // [n||] cp IHcp. - move/IHcp=> {IHcp}; apply: etrans; set G := cpmap cp. rewrite cpring_ecpR /rot !insertE_cat -catA uniq_catCA catA /=. by rewrite -insertE_cat cat_take_drop. - rewrite cpring_ecpY; case Dcp: cp => [|s cp']; first by rewrite cpring0. rewrite -{s cp'}Dcp; set G := cpmap cp => /IHcp {}IHcp. rewrite 2!cat_cons (insertE_cat [:: _; _]) -map_cons -map_cat. rewrite insertE_icpY cat_uniq has_map has_pred0 !andTb. rewrite (map_inj_uniq (@icpY_inj G G)) -cat1s !insertE_cat uniq_catCA. by rewrite -!insertE_cat catA -[h in h ++ _]head_cpring. move=> cp_ok; move/(_ cp_ok): IHcp. have:= cpmap_proper (config_prog_cubic cp_ok); set G := cpmap cp => Ggt1 IHcp. rewrite (cpring_ecpH Ggt1) insertE_cat [p in _ ++ p](insertE_cat [:: _]). rewrite uniq_catCA (insertE_cat [:: _; _]) -catA -insertE_cat catA. rewrite -!map_cons -map_cat insertE_icpH [node _]/= if_neg [_ == _]/= nodeK. rewrite (negPf Ggt1) cat_uniq has_map has_pred0 (map_inj_uniq (@icpH_inj G G)). rewrite andTb insertE_cat (insertE_cat [:: _; _]) uniq_catCA -!insertE_cat. by rewrite catA -[h in h ++ _]head_proper_cpring. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring cfmap ctree) fourcolor(cfcolor)