proposition: Theorem FpredUlpPos : forall x : float, Fcanonic radix b x -> (0 < x)%R -> (FPred b radix precision x + Fulp b radix precision (FPred b radix precision x))%R = x.
proof: Proof. intros x Hx H. apply sym_eq; apply Rplus_eq_reg_l with (- FtoRradix (FPred b radix precision x))%R. apply trans_eq with (Fulp b radix precision (FPred b radix precision x)); [ idtac | ring ]. apply trans_eq with (FtoRradix x - FtoRradix (FPred b radix precision x))%R; [ ring | idtac ]. unfold FtoRradix in |- *; rewrite <- Fminus_correct; auto with zarith; fold FtoRradix in |- *. pattern x at 1 in |- *; replace x with (FSucc b radix precision (FPred b radix precision x)); [ idtac | apply FSucPred; auto with zarith arith ]. unfold FtoRradix in |- *; apply FSuccUlpPos; auto with zarith arith. apply FPredCanonic; auto with zarith arith. apply R0RltRlePred; auto with zarith arith real. Qed.
imports: Reals ZArith List PeanoNat Psatz