proposition: Lemma size_walkq x q : size (walkq x q) = size (flatq q).
proof: Proof. by elim: q x => //= *; rewrite ?size_cat; congr _.+1; auto. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry coloring)