proposition: Lemma contains_fromZ_lower_upper z1 z2 i : (-256 <= z1 <= 0)%Z -> (0 <= z2 <= 256)%Z -> contains (I.convert (I.mask (I.bnd (I.lower (I.fromZ_small z1)) (I.upper (I.fromZ_small z2))) i)) (Xreal 0).
proof: Proof. move=> z1N z2P. apply: I.mask_correct'. rewrite I.bnd_correct. refine (_ (I.fromZ_small_correct z1 _) (I.fromZ_small_correct z2 _)) ; [|lia..]. move=> Hz2 Hz1. rewrite I.lower_correct; [|now exists (IZR z1)]. rewrite I.upper_correct; [|now exists (IZR z2)]. move: Hz2 Hz1. set i1 := I.convert _. set i2 := I.convert _. assert (H1 := IZR_le _ _ (proj2 z1N)). assert (H2 := IZR_le _ _ (proj1 z2P)). case: i1 => [|[|x1] [|x2]] /=; case: i2 => [|[|x3] [|x4]] //=; lra. apply: I.valid_lb_lower; exists (IZR z1); apply I.fromZ_small_correct; lia. apply: I.valid_ub_upper; exists (IZR z2); apply I.fromZ_small_correct; lia. Qed.
imports: Coq(Reals ZArith Psatz) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq bigop) Interval Xreal Basic Interval_compl Datatypes Taylor_model_sharp Bound Bound_quad Univariate_sig