proposition: Lemma match_gram_rot et w : matchg [::] (rot 1 et) (gram_rot w) = matchg [::] et w.
proof: Proof. rewrite /gram_rot; case: ifPn => [/existsP[/= b0]| ]; last first. rewrite negb_exists => /forallP/(_ _)/negPf /= bal'w. by apply/idP/idP=> /matchg_balanced[_]; rewrite bal'w. case: et w => [|e et]; first by do 4!case=> //. rewrite rot1_cons => [[|[] w]] /= bal_w; try by case: e et; do 2?case. suffices{bal_w} IHw b lb: gram_balanced (size lb) b0 w -> matchg (b :: lb) (rcons et e) (rcons w Gpop1) = (e == ccons true (~~ last b lb)) && matchg (belast b lb) et w. - by rewrite match_gram_flip !{}IHw //; case: e; rewrite ?orbF. rewrite andbC; elim: w lb b b0 et => [|s w IHw] lb b b0 et. by case: lb => // [] _; case: b; (case: et; [case: e | do 2?case]). case: et => [|e' et]; first by case: s; case: e {IHw} => //; case: b; case: w. case: s; case: e' => //=; by [ apply: IHw | apply: (IHw (b :: lb)) | case: b; case: lb => [|b' lb] //=; apply: IHw]. elim: w [::] et {b0 bal_w} => [|s w IHw] lb et. by case e; case: et; do 2?case. case: et => [|e' et]; first by case e; case: s lb => [|||] [|[|] lb] //; case w. by case: s; case: e' => //=; case: lb => [|[|] lb'] //=; case e. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap walkup jordan geometry color chromogram) fourcolor(coloring)