proposition: Lemma planar_ecpN : planar ecpN.
proof: Proof. have oFX: fcard face ecpN = fcard face G. exact: (adjunction_n_comp _ cfaceC cfaceC _ adjnF_ecpN). have geoX: ucycle_plain_quasicubic_connected (rev (cpring ecpN)). split; [split; last exact: ucycle_rev_cpring | exact connected_ecpN ]. by split; [ apply plain_ecpN | apply cubic_ecpN ]. rewrite (quasicubic_Euler geoX) oFX card_ecp /nilp size_rev size_cpring_ecpN. have:= planarG; rewrite (quasicubic_Euler geoG) size_rev head_proper_cpring //=. by rewrite /nilp size_rev !add1n !doubleS !addnS. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color)