proposition: Lemma same_halfg d1 d2 : halfg d1 = halfg d2 -> d2 \in traject gface d1 4.
proof: Proof. have Ed d: halfg d = halfg d2 -> (d2 == d) = (oddg d2 == oddg d). by move=> Ed; rewrite -[RHS](inj_eq (addrI (halfg d *+ 2))) halfgK Ed halfgK. by move=> Ed12; rewrite !inE !Ed ?halfg_face // !oddg_face; do 2!case: oddgP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div choice order ssralg ssrnum ssrint intdiv) fourcolor(hypermap)