proposition: Lemma Rexists_between : forall r1 r2, r1 < r2 -> exists r, r1 < r < r2.
proof: Proof. intros r1 r2 r1_lt_r2. exists ((r1 + r2) / 2). now apply Rlt_half_plus. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField