proposition: Lemma in_clink_glink (G : hypermap) (A : pred G) (plainG : plain G) : fclosed node A -> {in A&, connect (restrict A clink) =2 connect (restrict A glink)}.
proof: Proof. move => clA x y xA yA. apply/idP/idP. - case/connectP => [p]. elim: p x xA => [x xA _ -> //|z p IHp x xA /=]. rewrite -!andbA => /and4P [_ zA xz pth_p lst_p]. apply: connect_trans (IHp _ zA pth_p lst_p) => {pth_p lst_p}. case/clinkP : xz xA zA => [->|<-] => xA zA. + apply: connect_mono. apply: sub_restrict. apply: in2W. exact: glinkN. rewrite in_connect_sym // ?connect1 //=. exact: cnodeC. + by apply connect1; rewrite /= xA zA /glink/= eqxx. - case/connectP => [p]. elim: p x xA => [x xA _ -> //|z p IHp x xA /=]. rewrite -!andbA => /and4P [_ zA xz pth_p lst_p]. apply: connect_trans (IHp _ zA pth_p lst_p) => {pth_p lst_p IHp}. gen have N,N': x z xA zA {xz} / node x == z -> connect (restrict A clink) x z. { move/eqP => E. rewrite -{}E in zA *. apply: connect_mono. apply: sub_restrict. apply: in2W. exact: sub_node_clink. rewrite in_connect_sym // ?connect1 //= ?xA ?zA ?finv_f ?eqxx //. * move => u v /eqP <-. by rewrite (clA (finv node u) u) //= f_finv. * by apply/fconnect_sym/finv_inj. } gen have F,F': x z xA zA {xz N N'} / face x == z -> connect (restrict A clink) x z. { move/eqP => E; rewrite -{}E in zA *. by apply: connect1; rewrite /= xA zA clinkF. } case/or3P : xz => //= {N' F'}. rewrite -plain_eq' => // /eqP => E; rewrite -{}E in zA *. have ? : face x \in A by rewrite (clA (face x) (node (face x))) //=. apply: connect_trans (N (face x) _ _ _ _) => //. exact: F. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) fourcolor(hypermap geometry jordan color coloring combinatorial4ct) GraphTheory(hmap_ops)