proposition: Lemma avg_half_sub_zero: a = 0 -> av = 0.
proof: Proof. Proof with auto with typeclass_instances. intros H. assert (y=-x). apply Rplus_eq_reg_l with x. apply Rmult_eq_reg_r with (/2). apply trans_eq with a. reflexivity. rewrite H; ring. lra. unfold av, avg_half_sub. rewrite H0. replace (-x-x) with (-(2*x)) by ring. rewrite round_generic with (x:=(-(2*x)))... replace (-(2*x)/2) with (-x) by field. rewrite round_generic with (x:=-x)... replace (x+-x) with 0 by ring. apply round_0... now apply generic_format_opp. apply generic_format_opp. now apply FLT_format_double. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Plus_error)