proposition: Lemma avg_naive_same_sign_2: a <= 0-> av <= 0.
proof: Proof. Proof with auto with typeclass_instances. intros H. rewrite avg_naive_correct. apply round_le_generic... apply generic_format_0. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Plus_error)