proposition: Lemma fitp_mirror p x : @exact_fitp G x (mirror_part p) = @exact_fitp (mirror G) x p.
proof: Proof. move Dars: (fun n G1 x => arity (edge (iter n face (@edge G1 x)))) => ars. have DarsG := fun n G1 x => erefl (ars n G1 x). move: {DarsG}(DarsG 2) (DarsG 3) (DarsG 4) (DarsG 5) x p. rewrite -{2 4 6 8}Dars /= => Dars2 Dars3 Dars4 Dars5. have Ears2 (x : G): ars 2 (mirror G) x = ars 2 G x. rewrite -{1}Dars arity_mirror /= arity_face. rewrite -[node x]nodeK -{1}[x]edgeK Dn3 !(finv_f faceI). rewrite -{1}[face (edge x)]faceK De2. by rewrite -{1}[face (face (edge x))]edgeK Dn3 arity_face -Dars2. have Earsf n m (x : G): arity (edge x) == m -> n <= m -> ars n (mirror G) (face x) = ars (m - n) G x. - move=> Dm Hnm; rewrite -{1}Dars /= -{1}[x]De2 edgeK. rewrite -arity_face in Dm; rewrite (iter_finv faceI) (eqP Dm) //. by rewrite -iterSr -(canRL edgeK (De2 _)) (order_finv faceI) arity_face -Dars. have Ears (x : G): arity (edge (face x : mirror G)) = arity (edge x). by rewrite arity_mirror /= -{1}[x]De2 edgeK arity_face. move: {Earsf}Ears Ears2 (Earsf 3) (Earsf 4) (Earsf 5). rewrite -{1 3 5 7}Dars /= => Ears Ears2 Ears3 Ears4 Ears5. have fit_ars G1 x p h0: @fitp G1 x p -> p = Pnil \/ next_hat h0 p (ars 2 _ x). by rewrite -Dars; case Dp: p; by [left | case/and3P; right]. move=> x p; rewrite /exact_fitp size_mirror_part arity_mirror /mirror_part. set h0 := get_hat p; pose h0hx := h0 (ars 2 _ x); symmetry. case: (arity x =P size_part p) => // nFx. pose sz0 q := size_part q == 0; set q := Pnil. transitivity (fitp x q && @fitp (mirror G) x p && (sz0 p || h0hx)). case fit_p: (@fitp (mirror G) x p); rewrite {nFx}//= {}/h0hx {}/h0. case: (fit_ars (mirror G) x p Pr59 fit_p) => [-> // | ]. by rewrite -{1}Dars /= Ears2 /= => h0x; apply/esym/orP; right. have Eqp: next_hat h0 q = next_hat h0 p by rewrite /h0; case p. have: sz0 q ==> (next_hat h0 q (ars 2 _ x) == h0hx) by apply: eqxx. clearbody h0; move: q Eqp; rewrite -{1 2 3}[x]iter_face_arity {}nFx /=. elim: p => [|s h p IHp|h f1 p IHp|h f2 f1 p IHp|h f3 f2 f1 p IHp] q /=; (rewrite ?andbT //; set y := iter (size_part p) face x => <- Dh0hx; rewrite Ears Ears2 -[RHS]IHp // -/y /=; rewrite -Dars2 -?Dars3 -?Dars4 -?Dars5 -?andbA; PopAnd fit_q; PopAnd Es; rewrite ?(Ears3 _ _ Es, Ears4 _ _ Es, Ears5 _ _ Es) // (finv_f faceI); rewrite andbC -(andbC h0hx) -?andbA [andb h0hx]lock; do ?bool_congr; rewrite andbC -lock andbA andbC; PopAnd fit_p; by transitivity h0hx; [ case: {fit_q}(fit_ars _ _ _ h0 fit_q) => [Dq | ->]; [rewrite {1}Dq /= in Dh0hx; rewrite (eqP Dh0hx) andbb | rewrite andbT] | case: {fit_p}(fit_ars _ _ _ h0 fit_p) => [Dp | ]; [ rewrite /y Dp /= andbT | rewrite -{1}Dars /= Ears2 /y => fit_p ; rewrite fit_p /=; case: (p) fit_p ] ]). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap color geometry)