proposition: Lemma average_between: Rmin x y <= av <= Rmax x y.
proof: Proof. Proof with auto with typeclass_instances. unfold av,a,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_between... rewrite Rmin_comm, Rmax_comm. apply avg_half_sub_between... apply avg_naive_between... apply avg_naive_between... case (Rle_bool_spec (Rabs x) (Rabs y)); intros. apply avg_half_sub_between... rewrite Rmin_comm, Rmax_comm. apply avg_half_sub_between... Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Plus_error)