proposition: Theorem F2R_Zabs: forall m e : Z, F2R (Float beta (Z.abs m) e) = Rabs (F2R (Float beta m e)).
proof: Proof. intros m e. unfold F2R. rewrite Rabs_mult. rewrite <- abs_IZR. simpl. apply f_equal. apply sym_eq; apply Rabs_right. apply Rle_ge. apply bpow_ge_0. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Digits