proposition: Lemma dscore_mirror (x : G) : @dscore (mirror G) x = dscore x.
proof: Proof. rewrite /dscore arity_mirror (eq_bigl _ _ (cface_mirror x)); congr (_ + _). suffices{x} score1F (x : G): @dscore1 (mirror G) (face x) = dscore1 x. rewrite (reindex_inj (@faceI G)) -(eq_bigl _ _ (fun y => cface1r y x)) /=. by apply: eq_bigr => y _; rewrite /dscore2 2!{1}score1F (plain_eq' geoG). rewrite /dscore1 /the_drules; congr _%:Z. elim: base_drules => [|p r IHp] //; pose n := size_part p. pose rp i := iter i (rot_part n.-1) (mirror_part p). have Erp i: size_part (rp i) = n. by elim: i => /= *; rewrite ?size_rot_part ?size_mirror_part. have fit_rp i G1 x1: @exact_fitp G1 x1 (rp i) = exact_fitp (iter i face x1) (mirror_part p). - elim: i {IHp} => //= i IHi in G1 x1 *. have [nFx1 | n'x1] := eqVneq (arity (face x1)) n. rewrite /= -{1}[x1](finv_f faceI) /finv nFx1 -fitp_rot ?Erp ?leq_pred //. by rewrite -iterS iterSr -IHi. rewrite /exact_fitp size_rot_part size_mirror_part Erp -/n. by rewrite !arity_face arity_iter_face in n'x1 *; rewrite (negPf n'x1). move Dp1: (rp 5%N) => p1. move: Dp1 {fit_rp}(fit_rp 5%N) {Erp}(Erp 5%N) => /= -> fit_p1 Ep1. set x2' := inv_face2 x; pose x3 := face (face (face x)). have Ex3: x3 = iter 5 face x2' by rewrite /x2' /inv_face2 /= !nodeK. rewrite /= !(f_finv nodeI) in IHp Ex3 *. case eq_pp1: (cmp_part p p1); rewrite //= {}IHp -/x2' -/x3; try by rewrite !fit_p1 // -Ex3 {1}Ex3 /= ?(finv_f faceI); rewrite -?(fitp_mirror geoG) mirror_mirror_part addnCA. congr ((_ : bool) + _)%N; apply/idP/idP=> /andP[Exp fit_xp]. have: @exact_fitp (mirror G) x3 p1. by rewrite /exact_fitp (fitp_cmp fit_xp) eq_pp1 /= andbT Ep1. rewrite fit_p1 Ex3 /= !(finv_f faceI). by rewrite -(fitp_mirror geoG) mirror_mirror_part. rewrite -(fitp_mirror geoG) Ex3 -fit_p1. by rewrite /exact_fitp (fitp_cmp fit_xp) eq_pp1 andbT Ep1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) mathcomp(bigop order ssralg ssrnum ssrint) fourcolor(hypermap geometry part)