proposition: Theorem inbetween_spec : (d <= x < u)%R -> inbetween inbetween_loc.
proof: Proof. intros Hx. unfold inbetween_loc. destruct (Rcompare_spec x d) as [H|H|H]. now elim Rle_not_lt with (1 := proj1 Hx). now constructor. constructor. now split. easy. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Float_prop