proposition: Lemma first_indices_increasing (u : nat -> R) (v : R -> nat) (H : enumeration R u v) : forall n : nat, n <> 0 -> v (fst (proj1_sig (tearing_sequences u v H n))) < v (fst (proj1_sig (tearing_sequences u v H (S n)))).
proof: Proof. intros. destruct n. - contradiction. - destruct (tearing_sequences u v H n) as [[r r0] H1] eqn:In. simpl in H1. destruct (tearing_sequences u v H (S n)) as [[r1 r2] H2] eqn:ISn. simpl in H2. destruct (tearing_sequences u v H (S (S n))) as [[r3 r4] H3] eqn:ISSn. simpl in H3. simpl. assert ((r1,r2) = first_two_in_interval u v r r0 H H1). { simpl in ISn. rewrite -> In in ISn. inversion ISn. reflexivity. } assert ((r3,r4) = first_two_in_interval u v r1 r2 H H2). { pose proof (tearing_sequences_projsig u v H (S n)). rewrite -> ISn in H5. rewrite -> ISSn in H5. apply H5. } pose proof (first_two_in_interval_works u v r r0 H H1) as firstChoiceWorks. rewrite <- H4 in firstChoiceWorks. destruct firstChoiceWorks as [fth [fth0 [fth1 [fth2 [fth3 fth4]]]]]. pose proof (first_two_in_interval_works u v r1 r2 H H2). rewrite <- H5 in H6. destruct H6 as [H6 [H7 [H8 [H9 [H10 H11]]]]]. apply fth4. + apply (Rlt_trans r r1); assumption. + apply (Rlt_trans r3 r2); assumption. + intro abs. subst. apply Rlt_irrefl in H6. contradiction. + intro abs. subst. apply Rlt_irrefl in H7. contradiction. Qed.
imports: Coq.Reals.Rdefinitions Coq.Reals.Raxioms Rfunctions Coq.Reals.RIneq Coq.Logic.FinFun Coq.Logic.ConstructiveEpsilon