proposition: Lemma avg_half_sub_no_underflow_aux2: forall u v, format u -> format v -> (0 <= u /\ 0 <= v) \/ (u <= 0 /\ v <= 0) -> u <= v -> (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 same_sign xLey H; unfold avg_half_sub. apply round_plus_neq_0... apply generic_format_round... intros J. assert (H1:x <= 0). apply Rplus_le_reg_r with (round_flt (round_flt (y - x) / 2)). rewrite J, Rplus_0_l. apply round_ge_generic... apply generic_format_0. unfold Rdiv; apply Rmult_le_pos. apply round_ge_generic... apply generic_format_0. apply Rplus_le_reg_l with x; now ring_simplify. lra. destruct H1 as [H1|H1]. destruct same_sign as [(H2,H3)|(_,H2)]. contradict H2; now apply Rlt_not_le. apply avg_half_sub_no_underflow_aux1 with (-x). now apply generic_format_opp. rewrite <- Ropp_0; now apply Ropp_lt_contravar. apply Rle_trans with (round_flt (round_flt (y - x) / 2)). apply Rplus_le_reg_l with x. rewrite J; right; ring. apply round_le... unfold Rdiv; apply Rmult_le_compat_r. lra. apply round_le_generic... now apply generic_format_opp. apply Rplus_le_reg_l with x. now ring_simplify. rewrite H1 in J, H. rewrite Rplus_0_l in H. contradict J; apply Rgt_not_eq, Rlt_gt. rewrite Rplus_0_l. unfold Rminus; rewrite Ropp_0, Rplus_0_r. rewrite round_generic with (x:=y)... apply Rlt_le_trans with (bpow emin). apply bpow_gt_0. apply round_ge_generic... apply generic_format_FLT_bpow... lia. apply Rle_trans with (1:=H). right; apply Rabs_right. apply Rle_ge; unfold Rdiv; apply Rmult_le_pos. rewrite <- H1; assumption. lra. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Plus_error)