proposition: Lemma average_same_sign_2: a <= 0-> av <= 0.
proof: Proof. Proof with auto with typeclass_instances. intros H; unfold av, average. case (Rle_bool_spec 0 x); case (Rle_bool_spec 0 y); intros. case (Rle_bool_spec (Rabs x) (Rabs y)); intros. apply avg_half_sub_same_sign_2... apply avg_half_sub_same_sign_2... now rewrite Rplus_comm. apply avg_naive_same_sign_2... apply avg_naive_same_sign_2... case (Rle_bool_spec (Rabs x) (Rabs y)); intros. apply avg_half_sub_same_sign_2... apply avg_half_sub_same_sign_2... now rewrite Rplus_comm. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Plus_error)