proposition: Lemma uhPos: (0 <= uh)%R.
proof: Proof. unfold FtoRradix; apply RleRoundedR0 with bo p (Closest bo radix) (ph+b)%R; auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. apply Rplus_le_reg_l with (-b)%R. ring_simplify. unfold FtoRradix; rewrite <- Fopp_correct; auto. apply RleBoundRoundl with bo p (Closest bo radix) (a*x)%R; auto with zarith. apply ClosestRoundedModeP with p; auto with zarith. apply oppBounded; auto. rewrite Fopp_correct; auto; fold FtoRradix; apply Rplus_le_reg_l with b. apply Rle_trans with 0%R; auto with real; rewrite Rplus_comm; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz