proposition: Lemma emb_ecard : fcard edge D = #|E(G)|.
proof: Proof. have ? : plain D by apply: emb_plain emb_f. rewrite /n_comp_mem (eq_card (predIT _)) //. apply/eqP; rewrite eqn_leq; apply/andP; split. - pose h (x : D) := [set f x; f (edge x)]. have h_inj : {in froots edge &, injective h}. { move=> x y root_x root_y. apply: contra_eq => xDy. have : ~~ cedge x y. rewrite -root_connect ?(eqP root_x) ?(eqP root_y) //. exact: fconnect_sym. apply: contraNneq; rewrite /h doubleton_eq_iff !(rwP eqP) -!emb_vertex //. case => [[?]|[]]; first by rewrite (negPf (simpleD _ _)). have [->|xDey] := eqVneq x (edge y); first by rewrite -cedge1. by move/(simpleD xDey)/negPf; rewrite plain_eq // => ->. } rewrite -(card_in_imset h_inj); apply: subset_leq_card. apply/subsetP => z /imsetP [x _ ->]. by rewrite in_edges -emb_edge ?adjn_edge. - have [e0 /edgesP [x0 _]|->] := picksP E(G); last by rewrite cards0. pose d0 := emb_inv x0. have link x y : x -- y -> { d : D | f d = x & f (edge d) = y }. { rewrite -[x]emb_invK -[y]emb_invK -emb_edge // => /existsP ex_d. exists (xchoose ex_d); apply/eqP; case/andP : (xchooseP ex_d) => ? ?. all: by rewrite -emb_vertex // cnodeC. } pose g (e : {set G}) : D := if edgeP e is Edge x y xy _ then froot edge (s2val (link x y xy)) else d0. have g_inj : {in E(G)&, injective g}. { move=> e1 e2 E1 E2; rewrite /g. case: (edgeP e1) => [x y xy ->|]; last by rewrite {1}E1. case: (edgeP e2) => [u v uv ->|]; last by rewrite {1}E2. case: (link x y xy) => d1 /= f_d1 f_ed1. case: (link u v uv) => d2 /= f_d2 f_ed2. move/eqP; rewrite root_connect; last exact: fconnect_sym. rewrite plain_orbit // !inE => /pred2P [?|?]; subst => //. by rewrite plain_eq // setUC. } rewrite -(card_in_imset g_inj); apply: subset_leq_card. apply/subsetP => z /imsetP [x E ->]; rewrite inE /g. case: edgeP => [*|] ; rewrite ?E ?roots_root //. exact: fconnect_sym. Qed.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry color coloring walkup combinatorial4ct cfmap) GraphTheory(edone preliminaries bij digraph sgraph) GraphTheory(connectivity minor hmap_ops smerge hcycle arc)