proposition: Lemma sign_lt_0 : forall x, x < 0 <-> sign x < 0.
proof: Proof. intros x. unfold sign. destruct total_order_T as [[H|H]|H] ; lra. Qed.
imports: Coq(Reals Psatz ssreflect) Coquelicot(Rcomplements Rbar Hierarchy Derive RInt Continuity Lim_seq ElemFct RInt_analysis)