proposition: Theorem truncate_0 : forall e l, let '(m', e', l') := truncate (0, e, l)%Z in m' = Z0.
proof: Proof. intros e l. unfold truncate. case Zlt_bool. simpl. apply Zdiv_0_l. apply refl_equal. Qed.
imports: Coq(ZArith Reals Lia) Core Digits Float_prop Bracket