proposition: Lemma fit_split_range k r : good_rsplit k r -> forall lo a, split_range k lo r a = (lo (+) (k < a)) && r a.
proof: Proof. by case: r => k_r [] a; move: k a k_r; do !case=> //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap color geometry)