proposition: Theorem inbetween_int_DN : forall x m l, inbetween_int m x l -> Zfloor x = m.
proof: Proof. intros x m l Hl. refine (Zfloor_imp m _ _). apply inbetween_bounds with (2 := Hl). apply IZR_lt. apply Zlt_succ. Qed.
imports: Coq(ZArith Reals Lia) Core Digits Float_prop Bracket