proposition: Lemma hombnd_rnd' : forall {m M u v b B}, hombnd' m M u v b B -> hombnd' (Rmin m M) M (round radix2 fxp ZnearestE u) v (round_err 53 b B) B.
proof: Proof. now apply hombnd_rnd. Qed.
imports: Reals Psatz Flocq(Core Operations Relative Plus_error)