fact: Definition lez m n := match m, n with | Posz m', Posz n' => (m' <= n')%N | Posz m', Negz n' => false | Negz m', Posz n' => true | Negz m', Negz n' => (n' <= m')%N end.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)