proposition: Lemma join_correct : forall ui vi u v x, contains (I.convert ui) (Xreal u) -> contains (I.convert vi) (Xreal v) -> (u <= x <= v)%R -> contains (I.convert (I.join ui vi)) (Xreal x).
proof: Proof. intros ui vi u v x Iu Iv [H1 H2]. assert (Hu := I.join_correct ui vi (Xreal u)). assert (Hv := I.join_correct ui vi (Xreal v)). destruct (I.convert (I.join ui vi)) as [|p q]. easy. split. destruct p as [|p]. easy. apply Rle_trans with (2 := H1). apply Hu. now left. destruct q as [|q]. easy. apply Rle_trans with (1 := H2). apply Hv. now right. Qed.
imports: Coq(Bool Reals Psatz) Coquelicot(Coquelicot) Stdlib Xreal Basic