proposition: Lemma source_drules_range : ~~ Pr58 nhub -> rs = [::].
proof: Proof. rewrite /rs /source_drules; case: rf => _ _ [] not_u58. have Eu: (fun p => size_part p == nhub) =1 (fun n => ~~ Pr58 n && (n == nhub)) \o size_part. - by move=> p; rewrite /= andbC; case: eqP => // ->. by rewrite /pick_source_drules (eq_filter Eu). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) mathcomp(bigop order ssralg ssrnum ssrint) fourcolor(hypermap geometry part)