fact: Definition gram_rot w := if [exists b, gram_balanced 0 b w] then match w with | Gpush :: w' => gram_flip (rcons w' Gpop1) | Gskip :: w' => rcons w' Gskip | _ => w end else w.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap walkup jordan geometry color chromogram) fourcolor(coloring)