proposition: Lemma avg_half_sub_symmetry_Ropp: forall u v, avg_half_sub (-u) (-v) = - avg_half_sub u v.
proof: Proof. intros u v; unfold avg_half_sub. replace (-v--u) with (-(v-u)) by ring. rewrite round_NE_opp. replace (- round_flt (v-u) / 2) with (- (round_flt (v-u) / 2)) by (unfold Rdiv; ring). rewrite round_NE_opp. replace (- u + - round_flt (round_flt (v - u) / 2)) with (-(u+round_flt (round_flt (v - u) / 2))) by ring. apply round_NE_opp. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Plus_error)