proposition: Lemma one_snum_subproof : Signed.spec 0 !=0 >=0 (1 : R).
proof: Proof. by rewrite /= oner_eq0 ler01. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)