proposition: Theorem inbetween_distance_inexact_abs : forall l, inbetween (loc_Inexact l) -> Rcompare (Rabs (d - x)) (Rabs (u - x)) = l.
proof: Proof. intros l Hl. rewrite Rabs_left1. rewrite Rabs_pos_eq. rewrite Ropp_minus_distr. now apply inbetween_distance_inexact. apply Rle_0_minus. apply Rlt_le. apply (inbetween_bounds _ Hl). apply Rle_minus. apply (inbetween_bounds _ Hl). Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Float_prop