proposition: Theorem inbetween_int_UP : forall x m l, inbetween_int m x l -> Zceil x = cond_incr (round_UP l) m.
proof: Proof. intros x m l Hl. assert (Hl': l = loc_Exact \/ (l <> loc_Exact /\ round_UP l = true)). case l ; try (now left) ; now right ; split. destruct Hl' as [Hl'|(Hl1, Hl2)]. rewrite Hl'. destruct Hl ; try easy. rewrite H. exact (Zceil_IZR _). rewrite Hl2. simpl. apply Zceil_imp. ring_simplify (m + 1 - 1)%Z. refine (let H := _ in conj (proj1 H) (Rlt_le _ _ (proj2 H))). apply inbetween_bounds_not_Eq with (2 := Hl1) (1 := Hl). Qed.
imports: Coq(ZArith Reals Lia) Core Digits Float_prop Bracket