proposition: Lemma planar_ecpU : planar ecpU.
proof: Proof. have oFX: fcard face ecpU = (fcard face G).+1. rewrite (n_compC (pred1 (ecpU : ecpU))) -add1n; congr (_ + _). by rewrite -(eq_n_comp_r cface_ecpU) (n_comp_connect cfaceC). by rewrite (adjunction_n_comp _ cfaceC cfaceC closedF_ecpU adjnF_ecpU). have geoX: ucycle_plain_quasicubic_connected (rev (cpring ecpU)). split; [split; last exact: ucycle_rev_cpring | exact connected_ecpU]. by split; [apply plain_ecpU | apply cubic_ecpU]. rewrite (quasicubic_Euler geoX) card_ecp oFX /nilp size_rev. rewrite size_cpring_ecpU add1n !doubleS !addSn 4!addnS mulnS !eqSS. by have:= planarG; rewrite (quasicubic_Euler geoG) /nilp size_rev head_cpring. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)