proposition: Lemma limit_index_above_all_indices (u : nat -> R) (v : R -> nat) (en : enumeration R u v) : forall n : nat, v (fst (proj1_sig (tearing_sequences u v en (S n)))) < v (proj1_sig (torn_number u v en)).
proof: Proof. intros. simpl. destruct (tearing_sequences u v en n) as [[r r0] H] eqn:tear. simpl. pose proof (first_two_in_interval_works u v r r0 en H). destruct (first_two_in_interval u v r r0) eqn:ft. simpl. assert (proj1_sig (tearing_sequences u v en (S n)) = (r1, r2)). { simpl. rewrite -> tear. assumption. } apply H0. - pose proof (torn_number_above_first_sequence u v en n). rewrite -> tear in H2. assumption. - pose proof (torn_number_below_second_sequence u v en n). rewrite -> tear in H2. assumption. - pose proof (torn_number_above_first_sequence u v en (S n)). rewrite -> H1 in H2. simpl in H2. intro H5. subst. apply Rlt_irrefl in H2. contradiction. - pose proof (torn_number_below_second_sequence u v en (S n)). rewrite -> H1 in H2. simpl in H2. intro H5. subst. apply Rlt_irrefl in H2. contradiction. Qed.
imports: Coq.Reals.Rdefinitions Coq.Reals.Raxioms Rfunctions Coq.Reals.RIneq Coq.Logic.FinFun Coq.Logic.ConstructiveEpsilon