proposition: Lemma refine_smatte_interpolant s (U V : region) (m : smatte) z : interpolant_at z U V m -> interpolant_at z U V (refine_smatte s m).
proof: Proof. case=> mz mU Vm; split=> [|t /mU-mt|t]; try exact/in_refine_smatte. by move/in_refine_smatte/Vm. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph bigop ssralg ssrnum ssrint) mathcomp(div intdiv) fourcolor(hypermap geometry coloring grid matte gridmap) fourcolor(real realplane realprop approx)