proposition: Lemma Posz_snum_subproof (xnz : nullity) (xr : reality) (x : {compare 0%N & xnz & xr}) : Signed.spec 0%Z xnz xr (Posz x%:num).
proof: Proof. by apply/andP; split; move: xr xnz x => [[[]|]|] []//=; move=> [[|x]//= _]. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)