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