proposition: Theorem sign_strict_correct : forall xi, match sign_strict xi with | Xeq => forall x, contains (convert xi) x -> x = Xreal 0 | Xlt => forall x, contains (convert xi) x -> x = Xreal (proj_val x) /\ Rlt (proj_val x) 0 | Xgt => forall x, contains (convert xi) x -> x = Xreal (proj_val x) /\ Rlt 0 (proj_val x) | Xund => True end.
proof: Proof. intros [|xl xu]. exact I. generalize (sign_strict_correct_ xl xu). unfold sign_strict. case (sign_strict_ xl xu); intro H; try exact I; (intros [|x]; [try easy; try now simpl; case (_ && _)|]); intro H'; [| |]. { now rewrite (proj1 (H _ H')). } { now split; simpl; [|elim (H _ H')]. } now split; simpl; [|elim (H _ H')]. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval