proposition: Lemma convert_bnd : forall l u v, contains (Ibnd l u) (I.F.convert v) -> contains (I.convert (I.bnd v v)) (I.F.convert v).
proof: Proof. intros l u v H. rewrite I.bnd_correct. destruct (I.F.convert v). elim H. split ; apply Rle_refl. - apply I.valid_lb_real. now revert H; case I.F.convert. - apply I.valid_ub_real. now revert H; case I.F.convert. Qed.
imports: Coq(Bool Reals) Flocq(Zaux Raux) Coq(List) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect) Stdlib Coquelicot Xreal Xreal_derive Basic Interval Interval_compl Taylor_model Tree Prog