proposition: Lemma double_snum_subproof nz r (x : {compare 0 & nz & r}) : Signed.spec 0 nz r x%:num.*2.
proof: Proof. by move: nz r x => [] [[[]|]|] [[|n]]. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)