proposition: Lemma in_refine_smatte s (m : smatte) z : refine_smatte s m z <-> m z.
proof: Proof. elim: s => // s <-; rewrite -[refine_smatte s m z]mem_approx_refine. by apply/eq_mem_approx=> t; rewrite /= in_refine_matte. 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)