proposition: Lemma sign_0_lt : forall x, 0 < x <-> 0 < sign x.
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)