proposition: Lemma match_gram_flip et w : matchg [::] et (gram_flip w) = matchg [:: true; false] et w || matchg [:: false; true] et w.
proof: Proof. set lb0 := [:: true; false]; set lb0' := [:: false; true]; set sb := [::]. rewrite /gram_flip -(cat0s lb0) -(cat0s lb0') -/sb -[0]/(size sb). elim: w et sb => [|s w IHw]; first by case=> [|[|||] [|e et]] [|b lb]. by case: s => [] [|[] et] [|[] lb] //=; rewrite !(orbF, IHw, match_gram_neg). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap walkup jordan geometry color chromogram) fourcolor(coloring)