proposition: Lemma avg_naive_between: Rmin x y <= av <= Rmax x y.
proof: Proof. Proof with auto with typeclass_instances. rewrite avg_naive_correct. split. apply round_ge_generic... now apply P_Rmin. apply Rmult_le_reg_l with (1 := Rlt_0_2). replace (2 * Rmin x y) with (Rmin x y + Rmin x y) by ring. replace (2 * a) with (x + y) by (unfold a; field). apply Rplus_le_compat. apply Rmin_l. apply Rmin_r. apply round_le_generic... now apply Rmax_case. apply Rmult_le_reg_l with (1 := Rlt_0_2). replace (2 * a) with (x + y) by (unfold a; field). replace (2 * Rmax x y) with (Rmax x y + Rmax x y) by ring. apply Rplus_le_compat. apply Rmax_l. apply Rmax_r. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Core Plus_error)