proposition: Lemma avg_half_sub_same_sign_2: a <= 0-> av <= 0.
proof: Proof. Proof with auto with typeclass_instances. intros H. apply round_le_generic... apply generic_format_0. apply Rplus_le_reg_l with (-x). ring_simplify. apply round_le_generic... now apply generic_format_opp. apply Rmult_le_reg_l with (1 := Rlt_0_2). apply Rle_trans with (-(2*x)). 2: right; ring. apply Rle_trans with (round_flt (y - x)). right; field. apply round_le_generic... apply generic_format_opp. now apply FLT_format_double... apply Rplus_le_reg_l with (2*x). apply Rmult_le_reg_r with (/2). lra. apply Rle_trans with 0;[idtac|right; ring]. apply Rle_trans with (2:=H). right; unfold a, Rdiv; ring. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Plus_error)