proposition: Lemma pred_round_le_id : forall rnd { Zrnd : Valid_rnd rnd } x, (pred (round beta fexp rnd x) <= x)%R.
proof: Proof. intros rnd Vrnd x. apply (Rle_trans _ (round beta fexp Raux.Zfloor x)). 2: now apply round_DN_pt. destruct (round_DN_or_UP beta fexp rnd x) as [Hr|Hr]; rewrite Hr. 2: now apply pred_UP_le_DN. apply pred_le_id. Qed.
imports: Coq(ZArith Reals Psatz) Zaux Raux Defs Round_pred Generic_fmt Float_prop