proposition: Lemma quasicubic_Euler : ucycle_plain_quasicubic_connected -> let nb_face := ~~ nilp r + fcard face G in planar G = (6 * nb_face == #|G| + ((size r).*2 + 12)).
proof: Proof. move=> [] [] [plainG cubicG] /andP[cycNr Ur] ccG. congr (is_true _); transitivity (6 * Euler_lhs G == 6 * Euler_rhs G). rewrite eqn_pmul2l // -(inj_eq double_inj) -(eqn_add2r (Euler_rhs G)). by rewrite -even_genusP. set szr := size r; set nbF := fcard face G. rewrite /Euler_rhs -/nbF; set nbE := fcard edge G; set nbN := fcard node G. have DnbE: #|G| = 2 * nbE. by apply: eqP; rewrite mulnC -(fcard_order_set edgeI plainG). have [nn DnbN Dnn]: exists2 nn, nbN = ~~ nilp r + nn & #|G| = szr + 3 * nn. exists (fcard node [predC r]). rewrite [nbN](n_compC (mem r)); congr (_ + _). case Dr: r => [|x r1]; first by apply: eq_card0 => x; rewrite !inE andbF. apply: etrans (n_comp_connect cnodeC x); apply/esym/eq_n_comp_r. by apply: fconnect_cycle; rewrite ?mem_head // -Dr. have clNr: fclosed node [predC r]. apply: predC_closed; apply: (intro_closed cnodeC) => /= x _ /eqP <- rx. by rewrite -(fconnect_cycle cycNr rx); apply: fconnect1. rewrite -[szr](card_uniqP Ur) -(cardC (mem r)); congr (_ + _); apply: eqP. by rewrite mulnC -(fcard_order_set nodeI cubicG). rewrite /Euler_lhs (eqnP ccG) mulnDr -[6 * _]/12 -{2}[6]/(1 + 2 + 3). rewrite 2!{1}mulnDl mul1n {2}Dnn {2}DnbE mulnDr !mulnA !mul2n muln2. rewrite (addnC nbN) DnbN !mulnDr 3!addnA addnC eqn_add2l addnA eqn_add2r. by rewrite -addnA addnC -addnA eq_sym addnC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap jordan)