proposition: Lemma succeed_by_split : let pl := split_part i j k lo p in let pr := split_part i j k (~~ lo) p in let p0l := if good_split i j k p0 then split_part i j k lo p0 else pl in good_split i j k p -> succeeds_in p0l pl -> (successful p0l -> succeeds_in p0 pr) -> succeeds_in p0 p.
proof: Proof. move=> pl pr p0l p_ijk pl_ok pr_ok p0p. have fitp_split x (x_ok : valid_hub x) := fitp_split (proj1 x_ok) _ _ x. have p0lpl: forced_part p0l pl. rewrite /p0l; case: ifP => [p0ijk | _] G x x_ok //. by rewrite !fitp_split // => /andP[-> /p0p->]. have {}pl_ok: successful pl by apply: pl_ok. have{p0lpl}pr_ok: successful pr. apply: pr_ok => G x x_ok => [|p0x]; have:= pl_ok G x x_ok. exact/contra/p0lpl. by rewrite !fitp_split // p0p ?andbT ?addNb. move=> G x x_ok; have []:= (pl_ok G x x_ok, pr_ok G x x_ok). by rewrite !fitp_split // addNb; case: (_ (+) _). 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)