proposition: Theorem UlpFlessuGe_aux : forall p : float, Fbounded b p -> Fcanonic radix b p -> (Rabs p - Fulp b radix precision p <= Rabs (FLess p))%R.
proof: Proof. intros p H H1. cut (forall p : float, Fbounded b p -> Fcanonic radix b p -> (0 < p)%R -> (Rabs p - Fulp b radix precision p <= Rabs (FPred b radix precision p))%R); [ intros V | idtac ]. unfold FLess in |- *; case (Rcase_abs p); intros H2. rewrite <- Rabs_Ropp; unfold FtoRradix in |- *; rewrite <- Fopp_correct. pattern p at 3 in |- *; rewrite <- Fopp_Fopp. rewrite <- (Rabs_Ropp (FtoR radix (FSucc b radix precision (Fopp (Fopp p))))); rewrite <- (Fopp_correct radix (FSucc b radix precision (Fopp (Fopp p)))). rewrite <- FPredFopFSucc with b radix precision (Fopp p); auto with zarith. replace (Fulp b radix precision p) with (Fulp b radix precision (Fopp p)). fold FtoRradix in |- *; apply V; auto. apply oppBounded; easy. apply FcanonicFopp; easy. unfold FtoRradix in |- *; rewrite Fopp_correct; auto with real. unfold Fulp in |- *; rewrite Fnormalize_Fopp; auto with zarith. cut (0 <= p)%R; [ intros H3; case H3; intros H4 | auto with real ]. apply V; auto. rewrite <- H4; rewrite Rabs_R0. ring_simplify (0 - Fulp b radix precision p)%R; apply Rle_trans with 0%R; auto with real zarith. rewrite <- Ropp_0; apply Ropp_le_contravar. now unfold Fulp; apply powerRZ_le, IZR_lt. apply Rabs_pos. intros q H2 H3 H4. unfold FtoRradix in |- *; rewrite <- FpredUlpPos with b radix precision q; auto with zarith; fold FtoRradix in |- *. apply Rle_trans with (Rabs (FtoRradix (FPred b radix precision q)) + Rabs (Fulp b radix precision (FPred b radix precision q)) - Fulp b radix precision q)%R; [ unfold Rminus in |- *; apply Rplus_le_compat_r; apply Rabs_triang | idtac ]. rewrite (Rabs_right (Fulp b radix precision (FPred b radix precision q))); [ idtac | apply Rle_ge; unfold Fulp in |- *; auto with real zarith ]. apply Rplus_le_reg_l with (Fulp b radix precision q). ring_simplify (Fulp b radix precision q + (Rabs (FtoRradix (FPred b radix precision q)) + Fulp b radix precision (FPred b radix precision q) - Fulp b radix precision q))%R. rewrite Rplus_comm; apply Rplus_le_compat_r. apply FulpFPredGePos; auto with zarith real. now apply powerRZ_le, IZR_lt. Qed.
imports: Reals ZArith List PeanoNat Psatz