proposition: Lemma nat_typ_subproof (x : nat) : Signed.spec 0%N ?=0 >=0 x.
proof: Proof. by []. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)