proposition: Lemma avg_half_sub_correct: (0 <= x /\ 0 <= y) \/ (x <= 0 /\ y <= 0) -> Rabs (av-a) <= 3/2 * ulp_flt a.
proof: Proof. Proof with auto with typeclass_instances. intros same_sign; case (Rle_or_lt x y); intros H. now apply avg_half_sub_correct_aux2. unfold av, a. rewrite <- (Ropp_involutive x), <- (Ropp_involutive y). rewrite avg_half_sub_symmetry_Ropp. rewrite <- Rabs_Ropp. replace (- (- avg_half_sub (- x) (- y) - (- - x + - - y) / 2)) with (avg_half_sub (-x) (-y) - ((-x+-y)/2)). 2: unfold Rdiv; ring. apply Rle_trans with (3 / 2 * ulp_flt ((- x + - y) / 2)). apply avg_half_sub_correct_aux2. now apply generic_format_opp. now apply generic_format_opp. apply Ropp_le_contravar; now left. rewrite <- Ropp_0; case same_sign; intros (T1,T2). right; split; now apply Ropp_le_contravar. left; split; now apply Ropp_le_contravar. right; apply f_equal. rewrite <- ulp_opp. apply f_equal. unfold Rdiv; ring. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Plus_error)