proposition: Lemma signed_le_total : total (<=%O : rel nR).
proof: Proof. by move=> x y; apply: real_comparable => /=. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool) mathcomp(ssrnat eqtype choice order ssralg ssrnum ssrint) mathcomp(mathcomp_extra)