proposition: Lemma posnum_subdef : (x != 0) && (0 <= x).
proof: Proof. by rewrite -lt_def. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)