fact: Definition refine_mring (mr : seq gpoint) : seq gpoint := flatten [seq [seq p *+ 2 + oddg d | p <- [:: d; gface d]] | d <- mr].
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path order ssralg ssrnum ssrint div intdiv) fourcolor(grid)