proposition: Theorem non_increasing_natural_sequence_has_limit : ∀ s, (∀ n, s (S n) ≤ s n) → ∃ m l, (∀ i, m ≤ i → s i = l).
proof: Proof. intros s Hs. remember (s O) as i eqn:Hi ; symmetry in Hi. apply Nat.eq_le_incl in Hi. revert s Hs Hi. induction i; intros. exists O, (s O). intros i _. induction i; [ apply eq_refl | ]. eapply eq_trans; [ | apply IHi ]. apply Nat.le_antisymm; [ apply Hs | ]. apply Nat.le_0_r in Hi. rewrite IHi, Hi; apply Nat.le_0_l. remember (λ j, (s j - s (S j))%nat) as t eqn:Ht . destruct (LPO t) as [H1| (n, P1)]; subst t. exists O, (s O). intros j _. induction j; [ apply eq_refl | ]. eapply eq_trans; [ | apply IHj ]. pose proof (H1 j) as H2. apply Nat.sub_0_le in H2. apply Nat.le_antisymm; [ apply Hs | ]. apply H2. remember (λ j, s (S n + j)%nat) as t eqn:Ht . assert (H1 : ∀ n, t (S n) ≤ t n). intros j; subst t. rewrite Nat.add_succ_r; apply Hs. assert (H2 : (t O ≤ i)%nat). subst t; rewrite Nat.add_0_r. assert (s n ≤ S i). clear P1 H1. induction n; [ apply Hi | ]. eapply le_trans; [ apply Hs | apply IHn ]. apply Nat.succ_le_mono. eapply Nat.lt_le_trans; [ | apply H ]. apply Nat.nle_gt. intros H2; apply P1. apply Nat.sub_0_le, H2. pose proof (IHi t H1 H2). destruct H as (m, (l, H3)). exists (S n + m)%nat, l. intros j Hjm. assert (H5 : (m ≤ j - S n)%nat). apply Nat.le_add_le_sub_l, Hjm. pose proof (H3 (j - S n)%nat H5) as H6. subst t. rewrite Nat.add_sub_assoc in H6. rewrite Nat.add_comm, Nat.add_sub in H6; apply H6. eapply Nat.le_trans; [ | apply Hjm ]. apply Nat.le_sub_le_add_l. rewrite Nat.sub_diag. apply Nat.le_0_l. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series