proposition: Lemma UP_odd_d_aux : forall z, (F2R d < z <= F2R u)%R -> Rnd_UP_pt (generic_format beta fexp) z (F2R u).
proof: Proof. Proof with auto with typeclass_instances. intros z Hz1. replace (F2R u) with (round beta fexp Zceil z). apply round_UP_pt... case (Rnd_DN_UP_pt_split _ _ _ _ Hd Hu (round beta fexp Zceil z)). apply generic_format_round... intros Y ; elim (Rlt_irrefl z). apply Rle_lt_trans with (2:=proj1 Hz1), Rle_trans with (2:=Y). apply round_UP_pt... intros Y; apply Rle_antisym; trivial. apply round_UP_pt... apply Hu. apply Hz1. Qed.
imports: Coq(ZArith Reals Psatz) Core Operations