proposition: Lemma in_refine_inset s b z : inset_srect b z -> inset_srect (refine_srect s b) z.
proof: Proof. by elim: s => // s IHs /IHs; apply/mem_approx_refine_inset. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype tuple path fingraph bigop order ssralg) mathcomp(ssrnum ssrint div intdiv) fourcolor(hypermap geometry coloring grid matte) fourcolor(real realplane) Coq(Setoid Morphisms) fourcolor(realsyntax realprop)