proposition: Theorem truncate_aux_comp : forall t k1 k2, (0 < k1)%Z -> (0 < k2)%Z -> truncate_aux t (k1 + k2) = truncate_aux (truncate_aux t k1) k2.
proof: Proof. intros ((m,e),l) k1 k2 Hk1 Hk2. unfold truncate_aux. destruct (inbetween_float_ex beta m e l) as (x,Hx). assert (B1 := inbetween_float_new_location _ _ _ _ _ _ Hk1 Hx). assert (Hk3: (0 < k1 + k2)%Z). change Z0 with (0 + 0)%Z. now apply Zplus_lt_compat. assert (B3 := inbetween_float_new_location _ _ _ _ _ _ Hk3 Hx). assert (B2 := inbetween_float_new_location _ _ _ _ _ _ Hk2 B1). rewrite Zplus_assoc in B3. destruct (inbetween_float_unique _ _ _ _ _ _ _ B2 B3). now rewrite H, H0, Zplus_assoc. Qed.
imports: Coq(ZArith Reals Lia) Core Digits Float_prop Bracket