proposition: Lemma oddg_add2 p d : oddg (p *+ 2 + d) = oddg d.
proof: Proof. by case: p d => xp yp [xd yd] /=; rewrite -!mulz2 !modzMDl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div choice order ssralg ssrnum ssrint intdiv) fourcolor(hypermap)