proposition: Lemma CanonicGeNormal: forall f, Fcanonic beta b f -> (bpow beta (-dExp b+p-1) <= Rabs (FtoR beta f))%R -> (Fnormal beta b f)%Z.
proof: Proof. intros f Cf H1. case Cf; trivial. intros (H2,(H3,H4)). contradict H1; apply Rlt_not_le. rewrite <- Fabs_correct. 2: apply radix_gt_0. unfold FtoR, Fabs; simpl. rewrite H3, <- bpow_powerRZ. apply Rlt_le_trans with (bpow beta (p-1)*bpow beta (-dExp b))%R. 2: rewrite <- bpow_plus. 2: right; f_equal; ring. apply Rmult_lt_compat_r. apply bpow_gt_0. apply Rmult_lt_reg_l with (IZR beta). apply IZR_lt, radix_gt_0. rewrite <- mult_IZR. apply Rlt_le_trans with (IZR (Z.pos (vNum b))). apply IZR_lt. rewrite <- (Z.abs_eq beta). now rewrite <- Zabs_Zmult. apply Zlt_le_weak, radix_gt_0. rewrite pGivesBound. rewrite IZR_Zpower_nat. rewrite <- bpow_1. rewrite <- bpow_plus. apply bpow_le. rewrite inj_abs; lia. Qed.
imports: Coq(Lia) Pff Core