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