proposition: Lemma sign_le (x y : R) : x <= y -> sign x <= sign y.
proof: Proof. intros Hx. unfold sign. case total_order_T as [[H|H]|H] ; case total_order_T as [[H'|H']|H'] ; lra. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)