proposition: Theorem bounded_correct : forall xi, bounded xi = true -> lower_bounded xi = true /\ upper_bounded xi = true.
proof: Proof. unfold bounded. intros [|xl xu] H. discriminate H. now apply andb_prop. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval