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