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