proposition: Lemma ltNz_nat m n : (- m%:Z < n) = (m != 0) || (n != 0).
proof: Proof. by move: m n=> [|?] []. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)