proposition: Theorem subset_contains : forall xi yi, subset xi yi -> subset' xi yi.
proof: Proof. intros xi yi. destruct yi as [|yl yu]. easy. destruct xi as [|xl xu]. easy. intros [H|H]; revert H. { case xl; [now simpl|]; intro rxl. case xu; [now simpl|]; intros rxu Hr [|x] H; [now simpl|]. exfalso; apply (Rlt_irrefl rxl); revert Hr; apply Rle_lt_trans. elim H; apply Rle_trans. } intros [H1 H2] [|v] Hv. easy. apply contains_le in Hv. apply le_contains. now apply le_lower_trans with (1 := H1). now apply le_upper_trans with (2 := H2). Qed.
imports: Coq(Bool Reals Psatz) Coquelicot(Coquelicot) Stdlib Xreal Basic