proposition: Lemma grid_leqn_anti g1 g2 : grid_leqn g1 g2 -> grid_leqn g2 g1 -> g1 = g2.
proof: Proof. elim: g1 g2 => [[]|a g1 IH [|b g2]] //= /andP[Ha Hg1] /andP[Hb Hg2]. by rewrite (IH g2) //; case: ltngtP Ha Hb => // ->. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)