proposition: Lemma first_two_in_interval_works (u : nat -> R) (v : R -> nat) (a b : R) (pen : enumeration R u v) (plow : Rlt a b) : let (c,d) := first_two_in_interval u v a b pen plow in Rlt a c /\ Rlt c b /\ Rlt a d /\ Rlt d b /\ Rlt c d /\ (forall x:R, Rlt a x -> Rlt x b -> x <> c -> x <> d -> v c < v x).
proof: Proof. intros. destruct (first_two_in_interval u v a b) as [r r0] eqn:ft. unfold first_two_in_interval in ft. pose proof (first_in_holed_interval_works u v a b b pen plow) as Wb. destruct (first_in_holed_interval u v a b b pen plow) as [first_index pr]. pose proof (first_in_holed_interval_works u v a b (u first_index) pen plow) as Wu. destruct pr as [[H1 [H3 H4]] H2]. destruct (first_in_holed_interval u v a b (u first_index) pen plow) as [second_index pr2]. destruct pr2 as [[H5 [H7 diff]] H6]. destruct pen as [_ pen2]. destruct (Rle_dec (u first_index) (u second_index)) as [lfs | nlfs]. - destruct (split_couple_eq ft); subst; repeat (split; [assumption | idtac]); split. + destruct (Rle_lt_or_eq_dec _ _ lfs). * assumption. * exfalso. apply diff. symmetry. apply e. + intros. rewrite -> pen2. apply Wb; try assumption. apply Rlt_not_eq; assumption. - destruct (split_couple_eq ft); subst; repeat (split; [assumption | idtac]); split. + apply Rnot_le_lt, nlfs. + intros. rewrite -> pen2. apply Wu; assumption. Qed.
imports: Coq.Reals.Rdefinitions Coq.Reals.Raxioms Rfunctions Coq.Reals.RIneq Coq.Logic.FinFun Coq.Logic.ConstructiveEpsilon