proposition: Lemma Iconst_true_correct i x : Iconst i = true -> contains (I.convert i) x -> x = Xlower (I.convert i).
proof: Proof. rewrite /Iconst. case E1 : I.bounded => // . have [/(I.lower_bounded_correct _) /= [F1 F2] /(I.upper_bounded_correct _) /= [F3 _]] := I.bounded_correct _ E1. intros H1 H2. have {H1} := I.subset_correct _ _ _ H2 H1. specialize (F2 (not_empty_contains _ _ H2)). rewrite F2 /=. rewrite I.bnd_correct. case E3 : x => [|r] //. elim. rewrite F1. intros H3 H4. apply f_equal. now apply Rle_antisym. exact: I.valid_lb_real. exact: I.valid_ub_real. 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