proposition: Lemma qNeg: (q <= 0)%R.
proof: Proof. unfold FtoRradix; apply RleRoundedLessR0 with b t (Closest b radix) (x -p)%R; auto with zarith. apply ClosestRoundedModeP with t; auto with zarith. apply Rplus_le_reg_l with (p)%R; ring_simplify. generalize ClosestMonotone; unfold MonotoneP; intros. unfold FtoRradix; apply H with b x (x * (powerRZ radix s + 1))%R; auto with zarith real. apply Rplus_lt_reg_r with (-x)%R; ring_simplify. apply Rle_lt_trans with (x*0)%R;[right;ring|apply Rmult_lt_compat_l;auto with real zarith]. apply powerRZ_lt, IZR_lt; lia. unfold FtoRradix; apply RoundedModeProjectorIdem with (P:=(Closest b radix)) (b:=b); auto. apply ClosestRoundedModeP with t; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz