proposition: Lemma fcard_gmnode : (bbw * bbh <= fcard node gmdart_map)%N.
proof: Proof. rewrite (n_compC gm_inner) addnC (@leq_add 0) // -2!leq_double. rewrite -garea_refine_rect -size_enum_grect. rewrite -[n in n.*2]muln2 doubleMr (fcard_order_set nodeI _ gm_inner_closed). rewrite cardE -(size_map val) uniq_leq_size ?enum_grect_uniq // => d. rewrite mem_enum_grect in_refine_rect => bb_d. by apply/imageP/(ex_intro2 _ _ (sub d _)); rewrite // gmgridE bb_d. apply/subsetP=> /= u bb_u; rewrite inE. have cyc_u: fcycle node (traject node u 4). rewrite [3%N]lock /= rcons_path fpath_traject -lock /= -val_eqE. by rewrite !val_gmnode ?gm_inner_node // -[gedge _]gface4 !gnodeK. rewrite (order_cycle cyc_u) ?mem_head // looping_uniq. have neq_node v: oddg v != oddg u -> v != u by apply: contraNneq => ->. rewrite /looping !inE !(inj_eq nodeI) !negb_or. by apply/and3P; split; apply/neq_node; rewrite !val_gmnode ?gm_inner_node // !(oddg_node, oddg_edge); case: oddgP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph order ssralg ssrnum ssrint) fourcolor(hypermap geometry color coloring patch snip grid) fourcolor(matte)