proposition: Theorem ClosestErrorExpStrict : forall (p q : float) (x : R), Fbounded b p -> Fbounded b q -> Closest b radix x p -> q = (x - p)%R :>R -> q <> 0%R :>R -> (Fexp q < Fexp p)%Z.
proof: Proof. intros. case (Zle_or_lt (Fexp p) (Fexp q)); auto; intros Z1. absurd (powerRZ radix (Fexp p) <= powerRZ radix (Fexp q))%R. 2: apply Rle_powerRZ; auto with real arith. apply Rgt_not_le. red in |- *; apply Rlt_le_trans with (2 * powerRZ radix (Fexp q))%R. apply Rltdouble; auto with real arith. apply powerRZ_lt, IZR_lt; lia. apply Rle_trans with (2 * Fabs q)%R. apply Rmult_le_compat_l; auto with real arith. replace (powerRZ radix (Fexp q)) with (FtoRradix (Float 1 (Fexp q))); auto. apply (RleFexpFabs radix); auto with real zarith. unfold FtoRradix, FtoR in |- *; simpl in |- *; ring. rewrite (Fabs_correct radix); auto with arith. replace (FtoR radix q) with (x - p)%R; auto. apply ClosestExp; auto. apply IZR_le; lia. Qed.
imports: Reals ZArith List PeanoNat Psatz