proposition: Lemma cface_end0g u v : cface u v = (end0g u == end0g v).
proof: Proof. apply/idP/eqP=> [/connectP[_ /fpathP[k ->] ->] | /same_end0g/trajectP[k]]. rewrite last_traject; elim: k => //= k IHk in u *. by rewrite !val_insubd !(fun_if end0g) !end0g_node !if_same. without loss: k u v / k \in iota 2 2. case: k => [|[|k]] IHk ltk Dv; first by have ->: v = u by apply/val_inj. by rewrite cfaceC (IHk 3%N) // Dv /= gnode4. by rewrite (IHk k.+2) ?mem_iota. have Gv := valP v; rewrite !inE => /pred2P[]-> _ /= Dv; rewrite /= Dv in Gv. case Gn3u: (iter 3 gnode u \in gmgrid). rewrite 2!cface1 eq_connect0 //; apply/val_inj; rewrite !val_insubd Gn3u. by rewrite gnode4 Gv. by rewrite cface1 eq_connect0 //; apply/val_inj; rewrite !val_insubd Gn3u Gv. by rewrite cface1 eq_connect0 //; apply/val_inj; rewrite val_insubd Gv. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph order ssralg ssrnum ssrint) fourcolor(hypermap geometry color coloring patch snip grid) fourcolor(matte)