proposition: Theorem subnormal_exponent : forall e x, (e <= fexp e)%Z -> generic_format x -> x = F2R (Float beta (Ztrunc (x * bpow (- fexp e))) (fexp e)).
proof: Proof. intros e x He Hx. pattern x at 2 ; rewrite Hx. unfold F2R at 2. simpl. rewrite Rmult_assoc, <- bpow_plus. assert (H: IZR (Zpower beta (cexp x + - fexp e)) = bpow (cexp x + - fexp e)). apply IZR_Zpower. unfold cexp. set (ex := mag beta x). generalize (exp_not_FTZ ex). generalize (proj2 (proj2 (valid_exp _) He) (fexp ex + 1)%Z). lia. rewrite <- H. rewrite <- mult_IZR, Ztrunc_IZR. unfold F2R. simpl. rewrite mult_IZR. rewrite H. rewrite Rmult_assoc, <- bpow_plus. now ring_simplify (cexp x + - fexp e + fexp e)%Z. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop