proposition: Lemma mcorner0 m q : q \in m -> mcorner m q = 0%N -> subpred (ltouch q) m.
proof: Proof. have negb_Ngt0 b: ~~ (~~ b > 0)%N = b by case: b. move=> mq /eqP; rewrite eqn0Ngt !(addn_gt0, double_gt0) !negb_or !{}negb_Ngt0. case: q => x y in mq *; rewrite /+%R /= !subr0 => /and3P[mq11 mq01 mq10] p. by rewrite -mem_enum_grect /= !zspan_dec_inc; apply/allP/and5P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path order ssralg ssrnum ssrint div intdiv) fourcolor(grid)