proposition: Lemma point_in_holed_interval_works (a b h : R) : Rlt a b -> let p := point_in_holed_interval a b h in Rlt a p /\ Rlt p b /\ p <> h.
proof: Proof. intros. unfold point_in_holed_interval in p. pose proof (middle_in_interval a b H). destruct H0. destruct (Req_dec_T h ((a + b) / INR 2)). - subst. pose proof (middle_in_interval a ((a + b) / INR 2) H0). destruct H2. split. + assumption. + split. * apply (Rlt_trans p ((a + b) / INR 2)%R). -- assumption. -- assumption. * apply Rlt_not_eq. assumption. - split. + assumption. + split. * assumption. * intro abs. subst. contradiction. Qed.
imports: Coq.Reals.Rdefinitions Coq.Reals.Raxioms Rfunctions Coq.Reals.RIneq Coq.Logic.FinFun Coq.Logic.ConstructiveEpsilon