proposition: Theorem truncate_correct_partial' : forall x m e l, (0 < x)%R -> inbetween_float beta m e x l -> (e <= cexp beta fexp x)%Z -> let '(m', e', l') := truncate (m, e, l) in inbetween_float beta m' e' x l' /\ e' = cexp beta fexp x.
proof: Proof. intros x m e l Hx H1 H2. unfold truncate. rewrite <- cexp_inbetween_float with (1 := Hx) (2 := H1) by now left. generalize (Zlt_cases 0 (cexp beta fexp x - e)). destruct Zlt_bool ; intros Hk. - split. now apply inbetween_float_new_location. ring. - apply (conj H1). lia. Qed.
imports: Coq(ZArith Reals Lia) Core Digits Float_prop Bracket