proposition: Lemma torn_number_above_first_sequence (u : nat -> R) (v : R -> nat) (en : enumeration R u v) : forall n : nat, Rlt (fst (proj1_sig (tearing_sequences u v en n))) (proj1_sig (torn_number u v en)).
proof: Proof. intros. destruct (torn_number u v en) as [torn i]. simpl. destruct (Rlt_le_dec (fst (proj1_sig (tearing_sequences u v en n))) torn). - assumption. - exfalso. destruct i. assert (Rlt torn (fst (proj1_sig (tearing_sequences u v en (S n))))). { apply (Rle_lt_trans torn (fst (proj1_sig (tearing_sequences u v en n)))). - assumption. - apply tearing_sequences_inc_dec. } clear r. specialize (H (fst (proj1_sig (tearing_sequences u v en (S n))))). assert (tearing_elem_fst u v en (fst (proj1_sig (tearing_sequences u v en (S n))))). { exists (S n). reflexivity. } specialize (H H2). assert (Rlt torn torn). { apply (Rlt_le_trans torn (fst (proj1_sig (tearing_sequences u v en (S n))))); assumption. } apply Rlt_irrefl in H3. contradiction. Qed.
imports: Coq.Reals.Rdefinitions Coq.Reals.Raxioms Rfunctions Coq.Reals.RIneq Coq.Logic.FinFun Coq.Logic.ConstructiveEpsilon