proposition: Lemma cpmap_cover cp : config_prog cp -> fband (cpring (cpmap cp) ++ cpker cp) =i cpmap cp.
proof: Proof. elim: cp => [|s cp IHcp] //=; case: s => // [n||] cp_ok u. - by rewrite cpring_ecpR fband_cat fband_rot -fband_cat IHcp. - rewrite cpring_ecpY !cat_cons !fband_cons orbCA; apply/orP. have [[x uFx] | XFu] := fband_icpY u; [ right | by left; rewrite cfaceC]. rewrite (same_connect_r cfaceC (cface_node_ecpY _)) -fband_cons. rewrite -map_cat -map_cons -cat_cons -head_cpring unfold_in. rewrite {u uFx}(eq_has (same_cface uFx)) has_map (eq_has (cface_icpY _ x)). by case: cp IHcp cp_ok x => // _ _ []; rewrite cpring0 /= connect0 ?orbT. have properG := cpmap_proper (config_prog_cubic cp_ok); set G := cpmap cp. rewrite cpring_ecpH // {2}head_proper_cpring // !(fband_cat, fband_cons). rewrite -!orbA orbCA (orbCA (u \in _)) -fband_cat -fband_cons. rewrite (same_connect_r cfaceC (cface_node_ecpH _)) // -fband_cons. rewrite -!cat_cons -!map_cons -head_proper_cpring // -map_cat; apply/orP. have[[x uFx] | Xfu] := fband_icpH u; [right | by left; rewrite cfaceC]. rewrite unfold_in (eq_has (same_cface uFx)) has_map (eq_has (cface_icpH G x)). exact: IHcp. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)