proposition: Lemma oddg_add d1 d2 : oddg (d1 + d2) = oddg (d2 + oddg d1).
proof: Proof. by rewrite -[d1 in LHS]halfgK addrAC -addrA oddg_add2. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div choice order ssralg ssrnum ssrint intdiv) fourcolor(hypermap)