proposition: Lemma middle_in_interval : forall a b : R, Rlt a b -> (a < (a + b) / INR 2 < b)%R.
proof: Proof. intros. assert (twoNotZero: INR 2 <> 0%R). { apply not_0_INR. intro abs. inversion abs. } assert (twoAboveZero : (0 < / INR 2)%R). { apply Rinv_0_lt_compat. apply lt_0_INR. apply le_n_S. apply le_S. apply le_n. } assert (double : forall x : R, Rplus x x = ((INR 2) * x)%R) by now intros x; rewrite S_INR, INR_1, Rmult_plus_distr_r, Rmult_1_l. split. - assert (a + a < a + b)%R. { apply (Rplus_lt_compat_l a a b). assumption. } rewrite -> double in H0. apply (Rmult_lt_compat_l (/ (INR 2))) in H0. + rewrite <- Rmult_assoc in H0. rewrite -> Rinv_l in H0. * simpl in H0. rewrite -> Rmult_1_l in H0. rewrite -> Rmult_comm in H0. assumption. * assumption. + assumption. - assert (b + a < b + b)%R. { apply (Rplus_lt_compat_l b a b). assumption. } rewrite -> Rplus_comm in H0. rewrite -> double in H0. apply (Rmult_lt_compat_l (/ (INR 2))) in H0. + rewrite <- Rmult_assoc in H0. rewrite -> Rinv_l in H0. * simpl in H0. rewrite -> Rmult_1_l in H0. rewrite -> Rmult_comm in H0. assumption. * assumption. + assumption. Qed.
imports: Coq.Reals.Rdefinitions Coq.Reals.Raxioms Rfunctions Coq.Reals.RIneq Coq.Logic.FinFun Coq.Logic.ConstructiveEpsilon