proposition: Lemma Rlt_half_plus : forall r1 r2, r1 < r2 -> r1 < (r1 + r2) / 2 < r2.
proof: Proof. pose proof Rlt_0_2 as two_gt_0. assert (E : forall r r', (r + r') / 2 * 2 = r + r'). { now intros r r'; rewrite Rdiv_plus_distr, Rmult_plus_distr_r, <-2Rmult_div_swap, 2Rmult_div_l by (now apply Rgt_not_eq). } intros r1 r2 r1_lt_r2; split; apply Rmult_lt_reg_r with (1 := two_gt_0); rewrite E, Rmult_comm, <-Rplus_diag. - now apply Rplus_lt_compat_l. - now apply Rplus_lt_compat_r. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField