proposition: Lemma tearing_sequences_ordered_forall (u : nat -> R) (v : R -> nat) (pen : enumeration R u v) : forall n m : nat, let In := proj1_sig (tearing_sequences u v pen n) in let Im := proj1_sig (tearing_sequences u v pen m) in Rlt (fst In) (snd Im).
proof: Proof. intros. destruct (tearing_sequences u v pen n) eqn:tn. simpl in In. destruct (tearing_sequences u v pen m) eqn:tm. simpl in Im. destruct (n ?= m) eqn:order. - apply Nat.compare_eq_iff in order. subst. rewrite -> tm in tn. inversion tn. subst. assumption. - apply Nat.compare_lt_iff in order. apply (Rlt_trans (fst In) (fst Im)). + remember (fun n => fst (proj1_sig (tearing_sequences u v pen n))) as fseq. pose proof (increase_seq_transit fseq). assert ((forall n : nat, (fseq n < fseq (S n))%R)). { intro n0. rewrite -> Heqfseq. pose proof (tearing_sequences_inc_dec u v pen n0). destruct (tearing_sequences u v pen (S n0)). simpl. destruct ((tearing_sequences u v pen n0)). apply H0. } specialize (H H0). rewrite -> Heqfseq in H. specialize (H n m order). rewrite -> tn in H. rewrite -> tm in H. simpl in H. apply H. + assumption. - apply Nat.compare_gt_iff in order. apply (Rlt_trans (fst In) (snd In)). + assumption. + remember (fun n => snd (proj1_sig (tearing_sequences u v pen n))) as sseq. pose proof (decrease_seq_transit sseq). assert ((forall n : nat, (sseq (S n) < sseq n)%R)). { intro n0. rewrite -> Heqsseq. pose proof (tearing_sequences_inc_dec u v pen n0). destruct (tearing_sequences u v pen (S n0)). simpl. destruct ((tearing_sequences u v pen n0)). apply H0. } specialize (H H0). rewrite -> Heqsseq in H. specialize (H m n order). rewrite -> tn in H. rewrite -> tm in H. apply H. Qed.
imports: Coq.Reals.Rdefinitions Coq.Reals.Raxioms Rfunctions Coq.Reals.RIneq Coq.Logic.FinFun Coq.Logic.ConstructiveEpsilon