proposition: Lemma avg_half_sub_no_underflow_aux3: forall u v, format u -> format v -> (0 <= u /\ 0 <= v) \/ (u <= 0 /\ v <= 0) -> (bpow emin) <= Rabs ((u+v)/2) -> avg_half_sub u v <> 0.
proof: Proof. Proof with auto with typeclass_instances. clear Fx Fy a av x y; intros x y Fx Fy. intros same_sign H. case (Rle_or_lt x y); intros H1. now apply avg_half_sub_no_underflow_aux2. rewrite <- (Ropp_involutive x); rewrite <- (Ropp_involutive y). rewrite avg_half_sub_symmetry_Ropp. apply Ropp_neq_0_compat. apply avg_half_sub_no_underflow_aux2. now apply generic_format_opp. now apply generic_format_opp. rewrite <- Ropp_0; case same_sign; intros (T1,T2). right; split; now apply Ropp_le_contravar. left; split; now apply Ropp_le_contravar. apply Ropp_le_contravar; now left. apply Rle_trans with (1:=H). rewrite <- Rabs_Ropp. right; apply f_equal. unfold Rdiv; ring. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Plus_error)