proposition: Lemma genus_cube : genus cube = genus G.
proof: Proof. move: plain_cube cubic_cube; unlock cube => plainQ cubicQ. have oQ: #|qmap| = 6 * #|G| by rewrite card_prod cardT enumT unlock. have oEQ: fcard edge qmap = 3 * #|G|. apply/eqP; rewrite -(@eqn_pmul2l 2) // mulnA mulnC -oQ. by rewrite (fcard_order_set edgeI) //; apply/subsetP. have oNQ: fcard node qmap = 2 * #|G|. apply/eqP; rewrite -(@eqn_pmul2l 3) // mulnA mulnC -oQ. by rewrite (fcard_order_set nodeI) //; apply/subsetP. have oFeQ: fcard edge G = n_comp qf aQe. exact: etrans (esym (adjunction_n_comp _ qfC cedgeC qFaQe qfAe)). have oFnQ: fcard node G = n_comp qf aQn. exact: etrans (esym (adjunction_n_comp _ qfC cnodeC qFaQn qfAn)). have oFfQ: fcard face G = n_comp qf aQf. exact: etrans (esym (adjunction_n_comp _ qfC cfaceC qFaQf qfAf)). have{oFeQ oFnQ oFfQ} oFQ: fcard face qmap = Euler_rhs G. rewrite /Euler_rhs oFeQ -[fcard _ _](cardID aQe); congr (_ + _). by apply: eq_card => u; rewrite !inE -andbA. rewrite -(cardID aQn) oFnQ oFfQ; congr (_ + _); apply: eq_card => u. by rewrite !inE -!andbA /= !andbA; apply: andb_id2r => /eqP->. by rewrite !inE andbT andbCA andbA -negb_or andbC. suffices{oQ oEQ oNQ oFQ} oGQ: n_comp glink qmap = n_comp glink G. rewrite {1}/genus /Euler_lhs /Euler_rhs oQ oEQ oNQ oFQ oGQ. by rewrite mulSn 2!addnA -mulnDl addnC subnDl. have g1eq y g_y G x := @same_connect1 _ _ (@glinkC G) x (y G x) (g_y G x). have {}g1eq := (g1eq _ glinkE, g1eq _ glinkN, g1eq _ glinkF). have [[cGG cGQ] [[g1e g1n] g1f]] := (@clinkC G, @clinkC qmap, g1eq). rewrite -!(eq_n_comp (@clink_glink _)) (adjunction_n_comp (tsI CTnf) _ cGG) //. apply: (intro_adjunction _ _ (fun x _ => tsE x)) => // [u _ | x _]. split=> [|v _]; last first. rewrite clink_glink => /clinkP[->{u} | <-{v}]. by case: v => [[] v] //=; rewrite -!g1eq. by case: u => [[] u] //=; rewrite glinkC -g1eq. case: u => o x /=; pose gQx o1 := gcomp (tsI o1 x : qmap) (tsI CTnf x). have gQx_e: gQx CTe by rewrite /gQx g1n g1f. have gQx_fe: gQx CTfe by rewrite /gQx g1e 3!g1f. by rewrite (@clink_glink qmap); case: o; do 3!rewrite // g1f. split=> // y; rewrite (@clink_glink qmap). case/clinkP=> [->{x} | <-{y}]; last by rewrite 4!g1f. apply: (@connect_trans _ _ (tsI CTn y)); last by rewrite 3!(g1f qmap). by rewrite (@glinkC qmap) (g1n qmap) 2!(g1f qmap). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring)