proposition: Lemma cmp0 x : unify_r (Real AnySign) cond -> (x0 >=< x%:num).
proof: Proof. case: x => [x /= /andP[]]. by move: cond nz => [[[]|]|] [] //= _; do ?[by move=> /eqP ->; rewrite comparablexx]; move=> sx; rewrite /Order.comparable sx// orbT. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)