proposition: Lemma interval_sign_correct : forall xl xu : R, (xl <= xu)%R -> interval_sign xl xu.
proof: Proof. intros xl xu H. case (Rlt_le_dec xu 0); intro H0. exact (Nsign _ _ (Rlt_le _ _ H0)). case (Rlt_le_dec xl 0); intro H1. exact (Msign _ _ (Rlt_le _ _ H1) H0). exact (Psign _ _ H1). Qed.
imports: Reals