proposition: Lemma mem_cmp_range (r1 : prange) n : r1 n -> forall r2 : prange, r2 n = cmp_range r1 r2 (r2 n).
proof: Proof. by do 9?case: n => [|n]; case: r1 => // _; case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap color geometry)