proposition: Theorem inbetween_distance_inexact : forall l, inbetween (loc_Inexact l) -> Rcompare (x - d) (u - x) = l.
proof: Proof. intros l Hl. inversion_clear Hl as [|l' Hl' Hx]. now rewrite Rcompare_middle. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Float_prop