proposition: Lemma halfgK d : halfg d *+ 2 + oddg d = d.
proof: Proof. by case: d => x y; congr (Gpoint _ _); rewrite -mulz2 -divz_eq. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div choice order ssralg ssrnum ssrint intdiv) fourcolor(hypermap)