proposition: Lemma dscore_roots : \sum_(x in froots face) @dscore G x = 120.
proof: Proof. set F := froots face; pose ten : int := 10%:R; rewrite -[RHS]/(ten *+ 12). transitivity (\sum_(x in F) (ten *+ 6 + \sum_(y in cface x) (dscore2 y - ten))). by apply: eq_bigr => x; rewrite sumrB addrA addrAC sumr_const -!mulrnA !natz. rewrite big_split /= (sumz_connect _ cfaceC) !sumrB !sumr_const !addrA. apply/eqP; rewrite subr_eq addrAC (reindex_inj edgeI) subrK -mulrnDr -!mulrnA. have <-: fcard face G = #|F| by apply: eq_card => x; apply: andbT. by rewrite eqr_nat eqn_mul2l addnC -cubic_Euler; apply: geoG. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) mathcomp(bigop order ssralg ssrnum ssrint) fourcolor(hypermap geometry part)