proposition: Theorem RoundedModeErrorExpStrict : forall P, RoundedModeP b radix P -> forall (p q : float) (x : R), Fbounded b p -> Fbounded b q -> P x p -> q = (x - p)%R :>R -> q <> 0%R :>R -> (Fexp q < Fexp p)%Z.
proof: Proof. intros P H p q x H0 H1 H2 H3 H4. apply Zlt_powerRZ with (e := IZR radix); try apply IZR_le; auto with real zarith. apply Rle_lt_trans with (FtoRradix (Fabs q)). replace (powerRZ radix (Fexp q)) with (FtoRradix (Float 1 (Fexp q))); unfold FtoRradix in |- *; [ apply RleFexpFabs; auto with arith | unfold FtoR in |- *; simpl in |- *; ring ]. rewrite (Fabs_correct radix); auto with zarith. fold FtoRradix in |- *; rewrite H3. apply Rlt_le_trans with (Fulp p); [ apply RoundedModeUlp with P; auto | unfold Fulp in |- * ]. apply Rle_powerRZ; try apply IZR_le; auto with real zarith. apply FcanonicLeastExp with radix b precision; auto with real zarith. apply sym_eq; apply FnormalizeCorrect; auto. apply FnormalizeCanonic; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz