proposition: Lemma avg_naive_correct_weak2: Rabs (av -a) <= 3/2*ulp_flt a.
proof: Proof. Proof with auto with typeclass_instances. apply Rle_trans with (1:=avg_naive_correct_weak1). apply Rmult_le_compat_r. unfold ulp; apply ulp_ge_0. lra. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Plus_error)