proposition: Lemma same_end0g d1 d2 : end0g d1 = end0g d2 -> d2 \in traject gnode d1 4.
proof: Proof. move/(congr1 (+%R^~ (- Gpoint 1 1))); rewrite !end0g_sub1 => /same_halfg. by rewrite !inE -!gnode_sub1 !(inj_eq (addIr _)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div choice order ssralg ssrnum ssrint intdiv) fourcolor(hypermap)