proposition: Lemma real_domain_typ_subproof (R : realDomainType) (x : R) : Signed.spec 0%R ?=0 >=<0 x.
proof: Proof. by rewrite /= -realE num_real. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)