proposition: Lemma zero_snum_subproof : Signed.spec 0 ?=0 =0 (0 : R).
proof: Proof. exact: eqxx. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)