proposition: Lemma eqLeep: (Fexp q <= Fexp p)%Z.
proof: Proof. apply Fcanonic_Rle_Zle with radix b t; auto with zarith. left; auto. left; auto. rewrite Rabs_left1;[idtac|fold FtoRradix; apply qNeg]. rewrite Rabs_right;[idtac|fold FtoRradix; apply Rle_ge; apply pPos]. rewrite <- Fopp_correct. generalize ClosestMonotone; unfold MonotoneP; intros. unfold FtoRradix; apply H with b (-(x-p))%R p; auto with zarith real. apply Rplus_lt_reg_r with (-p)%R; ring_simplify;auto with real. apply ClosestOpp; auto. unfold FtoRradix; apply RoundedModeProjectorIdem with (P:=(Closest b radix)) (b:=b); auto. apply ClosestRoundedModeP with t; auto with zarith. elim Np; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz