proposition: Lemma num_abs_lt a x : 0 <= a -> (`|a|%:nng < x) = (a < x%:num).
proof: Proof. by move=> a0; rewrite -num_lt/= ger0_norm. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)