fact: Definition split_part i j k lo p := let p1 := take_part j p in let p2 := drop_part j p in let mkp df r p' := cat_part p1 (df (split_range k lo r) p') in match i, p2 with | Pspoke, Pcons s h p' => mkp (fun r => Pcons r h) s p' | Phat, Pcons s h p' => mkp (fun r => Pcons s r) h p' | Phat, Pcons6 h f1 p' => mkp (fun r => Pcons6 r f1) h p' | Phat, Pcons7 h f1 f2 p' => mkp (fun r => Pcons7 r f1 f2) h p' | Phat, Pcons8 h f1 f2 f3 p' => mkp (fun r => Pcons8 r f1 f2 f3) h p' | Pfan1, Pcons6 h f1 p' => mkp (fun r => Pcons6 h r) f1 p' | Pfan1, Pcons Pr66 h p' => mkp (fun r => Pcons6 h r) Pr59 p' | Pfan1, Pcons7 h f1 f2 p' => mkp (fun r => Pcons7 h r f2) f1 p' | Pfan1, Pcons Pr77 h p' => mkp (fun r => Pcons7 h r Pr59) Pr59 p' | Pfan1, Pcons8 h f1 f2 f3 p' => mkp (fun r => Pcons8 h r f2 f3) f1 p' | Pfan1, Pcons Pr88 h p' => mkp (fun r => Pcons8 h r Pr59 Pr59) Pr59 p' | Pfan2, Pcons7 h f1 f2 p' => mkp (fun r => Pcons7 h f1 r) f2 p' | Pfan2, Pcons Pr77 h p' => mkp (fun r => Pcons7 h Pr59 r) Pr59 p' | Pfan2, Pcons8 h f1 f2 f3 p' => mkp (fun r => Pcons8 h f1 r f3) f2 p' | Pfan2, Pcons Pr88 h p' => mkp (fun r => Pcons8 h Pr59 r Pr59) Pr59 p' | Pfan3, Pcons8 h f1 f2 f3 p' => mkp (fun r => Pcons8 h f1 f2 r) f3 p' | Pfan3, Pcons Pr88 h p' => mkp (fun r => Pcons8 h Pr59 Pr59 r) Pr59 p' | _, _ => p end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap color geometry)