proposition: Lemma num_eq0 x : (x%:num == 0) = (x == (widen_signed 0%:sgn : nR)).
proof: Proof. by []. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)