proposition: Lemma LSB_Pred: forall x y:float, (Rabs x < Rabs y)%R -> (LSB radix x <= LSB radix y)%Z -> (Rabs x <= Rabs y - powerRZ radix (LSB radix x))%R.
proof: Proof. intros. assert (exists nx:Z, (Rabs x=nx*powerRZ radix (LSB radix x))%R). unfold FtoRradix; rewrite <- Fabs_correct; auto. elim LSB_rep_min with radix (Fabs x); auto. intros nx H1; exists nx; rewrite H1. rewrite <- LSB_abs; auto. assert (exists ny:Z, (Rabs y=ny*powerRZ radix (LSB radix x))%R). unfold FtoRradix; rewrite <- Fabs_correct; auto. elim LSB_rep_min with radix (Fabs y); auto. intros ny1 H2; exists (ny1*Zpower_nat radix (Z.abs_nat (LSB radix y - LSB radix x)))%Z; rewrite H2. rewrite <- LSB_abs; auto; rewrite mult_IZR; unfold FtoR; simpl; unfold FtoR; simpl. rewrite Zpower_nat_Z_powerRZ. rewrite Rmult_assoc; rewrite <- powerRZ_add; auto with real zarith. replace (Z.abs_nat (LSB radix y - LSB radix x)+LSB radix x)%Z with (LSB radix y); auto with real. rewrite <- Zabs_absolu; rewrite Z.abs_eq; auto with zarith. apply IZR_neq; lia. apply Rplus_le_reg_l with (powerRZ radix (LSB radix x)-Rabs x)%R. ring_simplify. elim H1; intros nx H1'; elim H2; intros ny H2'; rewrite H1'; rewrite H2'. apply Rle_trans with ((IZR 1)*powerRZ radix (LSB radix x))%R;[simpl; right; ring|idtac]. apply Rle_trans with ((ny-nx)*powerRZ radix (LSB radix x))%R;[idtac|simpl; right; ring]. apply Rmult_le_compat_r; auto with real zarith. assert (ny-nx=(ny-nx)%Z)%R. unfold Zminus; rewrite plus_IZR; rewrite Ropp_Ropp_IZR; auto with real zarith. apply powerRZ_le, IZR_lt; lia. rewrite <- minus_IZR; apply IZR_le. assert (0 < ny - nx)%Z; auto with real zarith. apply lt_IZR; rewrite minus_IZR. apply Rplus_lt_reg_r with nx. ring_simplify. apply Rmult_lt_reg_l with ( powerRZ radix (LSB radix x)); auto with real zarith. apply powerRZ_lt, IZR_lt; lia. rewrite Rmult_comm; rewrite <- H1'; rewrite Rmult_comm; rewrite <- H2'; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz