proposition: Lemma avg_half_sub_between: Rmin x y <= av <= Rmax x y.
proof: Proof. Proof with auto with typeclass_instances. case (Rle_or_lt x y); intros M. rewrite Rmin_left; try exact M. rewrite Rmax_right; try exact M. now apply avg_half_sub_between_aux. rewrite Rmin_right; try now left. rewrite Rmax_left; try now left. unfold av; rewrite <- (Ropp_involutive x); rewrite <- (Ropp_involutive y). rewrite avg_half_sub_symmetry_Ropp. split; apply Ropp_le_contravar. apply avg_half_sub_between_aux. now apply generic_format_opp. now apply generic_format_opp. apply Ropp_le_contravar; now left. apply avg_half_sub_between_aux. now apply generic_format_opp. now apply generic_format_opp. apply Ropp_le_contravar; now left. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Plus_error)