proposition: Lemma succeed_by_similarity : let p1 := if mir then mirror_part p else p in let p2 := rot_part j p1 in size_part ps = size_part p2 /\ cmp_part p2 ps = Psubset -> succeeds_in p0 p.
proof: Proof. move=> p1 p2 [Eps2 eq_p2ps] _ G x x_ok; apply/negP => fit_p. pose G1 := if mir then mirror G else G. have [x1 x1ok Exp1]: exists2 x1 : G1, valid_hub x1 & exact_fitp x1 p1. have [cexG pos_x] := x_ok; rewrite /G1 /p1. case mir; last by exists x. exists x; last by rewrite -(fitp_mirror cexG) mirror_mirror_part. split; first exact: minimal_counter_example_mirror. by rewrite (dscore_mirror cexG). suffices [x2 x2ok Exp2]: exists2 x2 : G1, valid_hub x2 & exact_fitp x2 p2. have [Ep2 fit_p2] := andP Exp2; case/negP: (ps_ok x2ok); rewrite /exact_fitp. by rewrite Eps2 Ep2 (fitp_cmp fit_p2 ps) eq_p2ps. have [ltnj | lejn] := ltnP (size_part p1) j. exists x1 => //; rewrite /exact_fitp size_rot_part; congr (_ && _): Exp1. rewrite -[in LHS](cat_take_drop_part j p1) !fitp_cat andbC. set p3 := drop_part j p1; suffices: size_part p3 == 0 by case: p3. by rewrite size_drop_part subn_eq0 ltnW. have [cexG1 fit_x1] := x1ok. exists (iter j face x1); last by rewrite /p2 -fitp_rot. by rewrite /valid_hub -(@dscore_cface _ x1) // fconnect_iter. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph bigop ssralg ssrnum ssrint) fourcolor(hypermap geometry patch coloring birkhoff embed) fourcolor(quiz quiztree part redpart discharge hubcap) fourcolor(cfmap cfcontract cfreducible configurations)