proposition: Lemma fitp_split i j k p : good_split i j k p -> forall lo (x : G), exact_fitp x (split_part i j k lo p) = (lo (+) fitc i j k x) && exact_fitp x p.
proof: Proof. move=> p_ok lo x; rewrite /exact_fitp size_split_part andbCA; congr (_ && _). move: p_ok; rewrite /split_part /good_split. have (pc): part_update pc i -> forall q r, size_part (drop_part j p) = size_part (pc r q) -> (forall y : G, fitp y (drop_part j p) = fitp y (pc r q)) -> good_rsplit k r -> let p1 := cat_part (take_part j p) (pc (split_range k lo r) q) in fitp x p1 = (lo (+) (k < arity (i G (iter j face x)))) && fitp x p. - move=> Dpci q r Eq fit_q kr_ok. move: (Dpci r q) (Dpci (split_range k lo r) q) => [Erp fit_rp] [Erq fit_rq]. rewrite -{2}(cat_take_drop_part j p) /= !fitp_cat; bool_congr. have <-: j = size_part (take_part j p). apply: (@addIn (size_part (drop_part j p))). rewrite -size_cat_part cat_take_drop_part size_drop_part subnKC //. by rewrite ltnW // -subn_gt0 -size_drop_part Eq Erp. rewrite fit_q; apply/idP/idP=> [/fit_rq[] | /andP[xk_ok /fit_rp[Er]]]. by rewrite fit_split_range // => /andP[-> Er] ->. by apply; rewrite fit_split_range // xk_ok. case: (drop_part j p) i => [|s h p1|h f1 p1|h f1 f2 p1|h f1 f2 f3 p1] [] //. - by move/(_ _ (updatePs h)); apply. - by move/(_ _ (updatePh s)); apply. - case: s => //. + by move/(_ _ (updateP6f1 h)); apply=> //= y; rewrite !pentaG. + by move/(_ _ (updateP7f1 h Pr59)); apply=> //= y; rewrite !pentaG. by move/(_ _ (updateP8f1 h Pr59 Pr59)); apply=> //= y; rewrite !pentaG. - case: s => //. + by move/(_ _ (updateP7f2 h Pr59)); apply=> //= y; rewrite !pentaG. by move/(_ _ (updateP8f2 h Pr59 Pr59)); apply=> //= y; rewrite !pentaG. - case: s => //. by move/(_ _ (updateP8f3 h Pr59 Pr59)); apply=> //= y; rewrite !pentaG. - by move/(_ _ (updateP6h f1)); apply. - by move/(_ _ (updateP6f1 h)); apply. - by move/(_ _ (updateP7h f1 f2)); apply. - by move/(_ _ (updateP7f1 h f2)); apply. - by move/(_ _ (updateP7f2 h f1)); apply. - by move/(_ _ (updateP8h f1 f2 f3)); apply. - by move/(_ _ (updateP8f1 h f2 f3)); apply. - by move/(_ _ (updateP8f2 h f1 f3)); apply. by move/(_ _ (updateP8f3 h f1 f2)); apply. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap color geometry)