proposition: Lemma torn_number_below_second_sequence (u : nat -> R) (v : R -> nat) (en : enumeration R u v) : forall n : nat, Rlt (proj1_sig (torn_number u v en)) (snd (proj1_sig (tearing_sequences u v en n))).
proof: Proof. intros. destruct (torn_number u v en) as [torn i]. simpl. destruct (Rlt_le_dec torn (snd (proj1_sig (tearing_sequences u v en n)))) as [l|h]. - assumption. - exfalso. assert (Rlt (snd (proj1_sig (tearing_sequences u v en (S n)))) torn). { apply (Rlt_le_trans (snd (proj1_sig (tearing_sequences u v en (S n)))) (snd (proj1_sig (tearing_sequences u v en n))) torn). - apply (tearing_sequences_inc_dec u v en n). - assumption. } clear h. assert (is_upper_bound (tearing_elem_fst u v en) (snd (proj1_sig (tearing_sequences u v en (S n))))). { intros x H0. destruct H0. subst. left. apply tearing_sequences_ordered_forall. } destruct i. apply H2 in H0. pose proof (Rle_lt_trans torn (snd (proj1_sig (tearing_sequences u v en (S n)))) torn H0 H). apply Rlt_irrefl in H3. contradiction. Qed.
imports: Coq.Reals.Rdefinitions Coq.Reals.Raxioms Rfunctions Coq.Reals.RIneq Coq.Logic.FinFun Coq.Logic.ConstructiveEpsilon