proposition: Lemma in_pmring : pmring =i [pred d | halfg d == p].
proof: Proof. move=> d; rewrite -[p]halfg_double [RHS]eq_sym. by apply/idP/eqP=> [/trajectP[i _ ->] | /same_halfg]; rewrite ?halfg_iter_face. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path order ssralg ssrnum ssrint div intdiv) fourcolor(grid)