proposition: Lemma cubic_patch : cubic G = cubicb Gd && cubicb [predC bGr].
proof: Proof. congr (is_true _); apply/idP/andP => [cubicG | [cubicGd cubicGr]]. have{cubicG} [Dn3 neq_n] := (cubic_eq cubicG, cubic_neq cubicG). do [split; apply/cubicP] => [xd _ | xr b'x]. by split; [apply Ihd; rewrite !hdN Dn3 | rewrite -(inj_eq Ihd) hdN neq_n]. split; last by rewrite -(inj_eq Ihr) hrN ?neq_n. by apply Ihr; rewrite !hrN ?Dn3 // -!(fclosed1 (predC_closed clNbGr)). apply/cubicP => x _; have [xdP | ] := boolP (x \in codom hd). by rewrite -(f_iinv xdP) -!hdN (inj_eq Ihd) cubic_eq ?cubic_neq. rewrite im_hd !inE => /norP[/negbNE/imageP[xr _ ->]]. rewrite -EbGr (mem_map Ihr) => b'xr; have [n3xr x'nxr] := cubicP cubicGr _ b'xr. by rewrite -!hrN -?(fclosed1 (predC_closed clNbGr)) // n3xr (inj_eq Ihr). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry jordan color coloring)