proposition: Lemma bimplybplusNorm: forall f:float, Fbounded b f -> (FtoRradix f <> 0)%R -> (exists g:float, (FtoRradix g=f)%R /\ Fnormal radix (plusExp b) g).
proof: Proof. intros. exists (Fnormalize radix (plusExp b) t f); split. unfold FtoRradix; rewrite FnormalizeCorrect; auto with zarith. cut (Fcanonic radix (plusExp b) (Fnormalize radix (plusExp b) t f)). intros H1; case H1; auto;intros H2. absurd (Rabs f < (firstNormalPos radix (plusExp b) t))%R. apply Rle_not_lt. unfold firstNormalPos. apply Rle_trans with (powerRZ radix (-(dExp b))). unfold FtoRradix, FtoR, plusExp, nNormMin; simpl. rewrite Zpower_nat_Z_powerRZ; rewrite <- powerRZ_add. replace (pred t + - ((dExp b + Npos (P_of_succ_nat (pred (pred t)))))%N)%Z with (-(dExp b))%Z; auto with real. apply trans_eq with (pred t + - (dExp b + (Zpos (P_of_succ_nat (pred (pred t))))))%Z. replace (Zpos (P_of_succ_nat (pred (pred t)))) with (Z_of_nat (nat_of_P (P_of_succ_nat (pred (pred t))))); lia. cut (forall (x:N) (y:positive), (x+(Zpos y)=(x +Npos y)%N)%Z). intros T; rewrite <- T; auto with zarith. intros;unfold Nplus. case x; auto with zarith. apply IZR_neq; lia. unfold FtoRradix; rewrite <- Fabs_correct; auto. apply Rle_trans with (1*(powerRZ radix (- dExp b)))%R; auto with real. unfold FtoR; apply Rmult_le_compat; auto with real zarith. apply powerRZ_le, IZR_lt; lia. unfold Fabs; simpl. cut ((Fnum f=0)%Z \/ (1 <= Z.abs (Fnum f))%Z). intros H3; case H3; auto with real zarith. intros H4; absurd (FtoRradix f=0)%R; auto with real. unfold FtoRradix, FtoR; rewrite H4; simpl; ring. apply IZR_le. case (Zle_or_lt 0%Z (Fnum f)); intros H3. case (Zle_lt_or_eq _ _ H3); lia. right; lia. apply Rle_powerRZ; auto with real zarith. apply IZR_le; lia. unfold Fabs; simpl; elim H; auto. unfold FtoRradix; rewrite <- FnormalizeCorrect with radix (plusExp b) t f; auto. rewrite <- Fabs_correct; auto. apply FsubnormalLtFirstNormalPos; auto with zarith. unfold plusExp; simpl; auto. apply FsubnormFabs; auto. rewrite Fabs_correct; auto with real. apply Rabs_pos. apply FnormalizeCanonic; auto with zarith. elim H; split; unfold plusExp; simpl; lia. Qed.
imports: Reals ZArith List PeanoNat Psatz