proposition: Lemma top_typ_subproof d (T : porderType d) (x0 x : T) : Signed.spec x0 ?=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)