proposition: Lemma err_init: forall x, err (round_flx x) x eps.
proof: Proof. Proof with auto with typeclass_instances. intros x. apply Rle_trans with (/ 2 * bpow (- prec + 1) * Rabs x). apply relative_error_N_FLX... right; apply f_equal2; auto. apply f_equal, f_equal; ring. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Relative Sterbenz Operations) Interval(Tactic)