proposition: Theorem FulpFPredLe : forall f : float, Fbounded b f -> Fcanonic radix b f -> (Fulp b radix precision f <= radix * Fulp b radix precision (FPred b radix precision f))%R.
proof: Proof. intros f Hf1 Hf2; unfold Fulp in |- *. replace (Fnormalize radix b precision f) with f; [ idtac | apply FcanonicUnique with (radix := radix) (b := b) (precision := precision); auto with arith zarith ]. 2: apply FnormalizeCanonic; auto with zarith. 2: apply sym_eq; apply FnormalizeCorrect; auto with arith zarith. replace (Fnormalize radix b precision (FPred b radix precision f)) with (FPred b radix precision f); [ idtac | apply FcanonicUnique with (radix := radix) (b := b) (precision := precision); auto with arith zarith ]. 2: apply FPredCanonic; auto with zarith. 2: apply FnormalizeCanonic; auto with zarith. 2: apply FBoundedPred; auto with zarith. 2: apply sym_eq; apply FnormalizeCorrect; auto with arith zarith. pattern (IZR radix) at 2 in |- *; replace (IZR radix) with (powerRZ radix 1); [ idtac | simpl in |- *; auto with arith zarith real ]. rewrite <- powerRZ_add; auto with zarith real. 2: apply IZR_neq; lia. apply Rle_powerRZ; try apply IZR_le; auto with zarith real. replace (1 + Fexp (FPred b radix precision f))%Z with (Z.succ (Fexp (FPred b radix precision f))); auto with zarith. unfold FPred in |- *. generalize (Z_eq_bool_correct (Fnum f) (- pPred (vNum b))); case (Z_eq_bool (Fnum f) (- pPred (vNum b))); intros H1; [ simpl in |- *; auto with zarith | idtac ]. generalize (Z_eq_bool_correct (Fnum f) (nNormMin radix precision)); case (Z_eq_bool (Fnum f) (nNormMin radix precision)); intros H2; [ idtac | simpl in |- *; auto with zarith ]. generalize (Z_eq_bool_correct (Fexp f) (- dExp b)); case (Z_eq_bool (Fexp f) (- dExp b)); intros H3; simpl in |- *; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz