proposition: Lemma avg_naive_correct_weak1: Rabs (av -a) <= /2*ulp_flt a.
proof: Proof. Proof with auto with typeclass_instances. rewrite avg_naive_correct. apply error_le_half_ulp... Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Plus_error)