proposition: Lemma plain_patch : plain G = plainb [predC bGd] && plainb Gr.
proof: Proof. congr (is_true _); apply/idP/andP => [plainG | [plainGd plainGr]]. have{plainG} [De2 neq_e] := (plain_eq plainG, plain_neq plainG). do [split; apply/plainP] => [xd b'xd | xr _]. split; last by rewrite -(inj_eq Ihd) hdE ?neq_e. by apply Ihd; rewrite !hdE ?De2 // -(predC_closed clEbGd (eqxx _)). by split; [apply Ihr; rewrite !hrE De2 | rewrite -(inj_eq Ihr) hrE neq_e]. apply/plainP=> x _; have [xrP|] := boolP (x \in codom hr). by rewrite -(f_iinv xrP) -!hrE (inj_eq Ihr) plain_eq // plain_neq. rewrite im_hr !inE => /norP[/negbNE/imageP[xd _ ->{x}]]. rewrite (mem_map Ihd) => b'xd; have [eexd xd'exd] := plainP plainGd _ b'xd. by rewrite -!hdE ?eexd ?(inj_eq Ihd) // -(predC_closed clEbGd (eqxx _)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry jordan color coloring)