proposition: Lemma DN_odd_d_aux : forall z, (F2R d <= z < F2R u)%R -> Rnd_DN_pt (generic_format beta fexp) z (F2R d).
proof: Proof. Proof with auto with typeclass_instances. intros z Hz1. replace (F2R d) with (round beta fexp Zfloor z). apply round_DN_pt... case (Rnd_DN_UP_pt_split _ _ _ _ Hd Hu (round beta fexp Zfloor z)). apply generic_format_round... intros Y; apply Rle_antisym; trivial. apply round_DN_pt... apply Hd. apply Hz1. intros Y ; elim (Rlt_irrefl z). apply Rlt_le_trans with (1:=proj2 Hz1), Rle_trans with (1:=Y). apply round_DN_pt... Qed.
imports: Coq(ZArith Reals Psatz) Core Operations