proposition: Lemma match_gram_neg b0 et w : matchg [:: b0] et (gram_neg w) = matchg [:: ~~ b0] et w.
proof: Proof. set sb := [::]; rewrite /gram_neg -[0]/(size sb) -![_ :: _]/(rcons sb _). elim: w et sb => [|s w IHw] et lb; first by case lb. case: s; (case: et => [|e et]; first by case lb); by [ have:= IHw et (_ :: lb); case: e => /= | case: e; case: lb => [|b lb]; rewrite /= ?if_neg ?IHw ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap walkup jordan geometry color chromogram) fourcolor(coloring)