proposition: Lemma round_repr_same_exp : forall m e, exists m', round beta fexp rnd (F2R (Float beta m e)) = F2R (Float beta m' e).
proof: Proof. Proof with auto with typeclass_instances. intros m e. set (e' := cexp beta fexp (F2R (Float beta m e))). unfold round, scaled_mantissa. fold e'. destruct (Zle_or_lt e' e) as [He|He]. exists m. unfold F2R at 2. simpl. rewrite Rmult_assoc, <- bpow_plus. rewrite <- IZR_Zpower by lia. rewrite <- mult_IZR, Zrnd_IZR... unfold F2R. simpl. rewrite mult_IZR. rewrite Rmult_assoc. rewrite IZR_Zpower by lia. rewrite <- bpow_plus. apply (f_equal (fun v => IZR m * bpow v)%R). ring. exists ((rnd (IZR m * bpow (e - e'))) * Zpower beta (e' - e))%Z. unfold F2R. simpl. rewrite mult_IZR. rewrite IZR_Zpower by lia. rewrite 2!Rmult_assoc. rewrite <- 2!bpow_plus. apply (f_equal (fun v => _ * bpow v)%R). ring. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations Relative