proposition: Lemma average_correct: Rabs (av -a) <= 3/2 * ulp_flt a.
proof: Proof. Proof with auto with typeclass_instances. unfold av,a,average. case (Rle_bool_spec 0 x); case (Rle_bool_spec 0 y); intros. case (Rle_bool_spec (Rabs x) (Rabs y)); intros. apply avg_half_sub_correct... rewrite Rplus_comm. apply avg_half_sub_correct... apply avg_naive_correct_weak2... apply avg_naive_correct_weak2... case (Rle_bool_spec (Rabs x) (Rabs y)); intros. apply avg_half_sub_correct... right; split; now left. rewrite Rplus_comm. apply avg_half_sub_correct... right; split; now left. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Plus_error)