fact: Definition good_split i j k p := match i, drop_part j p with | Pspoke, Pcons s _ _ => good_rsplit k s | Phat, Pcons s h _ => good_rsplit k h | Phat, Pcons6 h _ _ => good_rsplit k h | Phat, Pcons7 h _ _ _ => good_rsplit k h | Phat, Pcons8 h _ _ _ _ => good_rsplit k h | Pfan1, Pcons6 _ f1 _ => good_rsplit k f1 | Pfan1, Pcons Pr66 _ _ => good_rsplit k Pr59 | Pfan1, Pcons7 _ f1 _ _ => good_rsplit k f1 | Pfan1, Pcons Pr77 _ _ => good_rsplit k Pr59 | Pfan1, Pcons8 _ f1 _ _ _ => good_rsplit k f1 | Pfan1, Pcons Pr88 _ _ => good_rsplit k Pr59 | Pfan2, Pcons7 _ _ f2 _ => good_rsplit k f2 | Pfan2, Pcons Pr77 _ _ => good_rsplit k Pr59 | Pfan2, Pcons8 _ _ f2 _ _ => good_rsplit k f2 | Pfan2, Pcons Pr88 _ _ => good_rsplit k Pr59 | Pfan3, Pcons8 _ _ _ f3 _ => good_rsplit k f3 | Pfan3, Pcons Pr88 _ _ => good_rsplit k Pr59 | _, _ => false end.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap color geometry)