proposition: Lemma nngE (x : sT) (unz : unify_nz ?=0 nz) (ucond : unify_r >=0 cond) : (widen_signed x%:num%:sgn unz ucond)%:num = x%:num.
proof: Proof. by []. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)