proposition: Lemma typ_snum_subproof d nz cond (xt : Signed.typ d nz cond) (x : Signed.sort xt) : Signed.spec (Signed.sort_x0 xt) nz cond x.
proof: Proof. by move: xt x => []. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)