proposition: Lemma cfctr_config_prog mr mc cp : cfctr mr mc cp ==> config_prog cp.
proof: Proof. elim: cp mr mc => //=; case=> // [n||] cp IHcp mr mc. - by case: (cfctr _ mc cp) (IHcp (rotr n mr) mc). - case Dcp: cp mr => [|s cp'] [|b1 [|b2 mr]] //. case: mr => [|b3 mr]; last by case: ifP. by case: mc => [|b3 mc] //; case: ifP. rewrite -{}Dcp; case: mc => [|b3 mc] //; case: ifP => // _. by case: (cfctr _ mc cp) (IHcp (b3 :: mr) mc). case: mr mc => [|b1 [|b2 mr]] [|b3 [|b4 [|b5 mc]]] //=. by do 2!case: ifP => // _; case: (cfctr _ mc cp) (IHcp [:: b4, b5 & mr] mc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring cfmap ctree) fourcolor(cfcolor)