proposition: Lemma Rle_half_plus : forall r1 r2, r1 <= r2 -> r1 <= (r1 + r2) / 2 <= r2.
proof: Proof. intros r1 r2 [I | ->]. - now split; left; apply (Rlt_half_plus r1 r2). - now split; rewrite Rdiv_plus_distr, Rplus_half_diag; apply Rle_refl. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField