proposition: Theorem non_increasing_natural_sequence_first_limit : ∀ s, (∀ n, s (S n) ≤ s n) → ∃ m l, (∀ i, m ≤ i → s i = l) ∧ (∀ i, i < m → l < s i)%nat.
proof: Proof. intros s Hs. generalize Hs; intros H. apply non_increasing_natural_sequence_has_limit in H. destruct H as (m, (l, H)). revert s Hs H. induction m; intros. exists O, l. split; [ apply H | ]. intros i Hi; exfalso; revert Hi; apply Nat.nlt_0_r. destruct (eq_nat_dec (s m) l) as [H1| H1]. assert (H2 : ∀ i, m ≤ i → s i = l). intros j Hmj. destruct (eq_nat_dec m j) as [H2| H2]; [ destruct H2; apply H1 | ]. apply Nat_le_neq_lt in H2; [ | apply Hmj ]. apply H, H2. pose proof IHm s Hs H2 as H3. destruct H3 as (m', (l', (H3, H4))). pose proof H2 (max m m') (Nat.le_max_l m m') as H5. pose proof H3 (max m m') (Nat.le_max_r m m') as H6. rewrite H5 in H6; clear H5; subst l'. exists m', l. split; [ intros i Hmi; apply H3, Hmi | ]. intros i Him'; apply H4, Him'. remember (λ j, s (S j)) as t eqn:Ht. assert (H2 : ∀ n, t (S n) ≤ t n) by (intros n; subst t; apply Hs). assert (H3 : ∀ i, m ≤ i → t i = l). intros j Hmj; subst t; apply H. apply Nat.succ_le_mono in Hmj; apply Hmj. pose proof IHm t H2 H3 as (m', (l', (H4, H5))). pose proof H3 (max m m') (Nat.le_max_l m m') as H7. pose proof H4 (max m m') (Nat.le_max_r m m') as H8. rewrite H7 in H8; subst l'; clear H7; subst t. destruct (lt_eq_lt_dec m m') as [[H6| H6]| H6]. pose proof H5 m H6 as H7. pose proof H3 m (Nat.le_refl m) as H8. rewrite H8 in H7. exfalso; revert H7; apply Nat.lt_irrefl. subst m'. exists (S m), l. split; [ intros i Hmi; apply H, Hmi | ]. intros i Him. destruct (eq_nat_dec i m) as [H6| H6]. subst i. apply Nat_le_neq_lt; [ | apply Nat.neq_sym, H1 ]. eapply le_trans; [ | apply Hs ]. apply Nat.eq_le_incl, Nat.eq_sym. apply H3, Nat.le_refl. apply Nat_le_neq_lt in H6; [ | apply Nat.succ_le_mono, Him ]. eapply Nat.lt_le_trans; [ apply H5, H6 | apply Hs ]. exists (S m'), l. split. intros i Hm'i. destruct i; [ exfalso; revert Hm'i; apply Nat.nle_succ_0 | ]. apply H4, Nat.succ_le_mono, Hm'i. intros i Him'. destruct m; [ exfalso; revert H6; apply Nat.nlt_0_r | ]. exfalso; apply H1, H4, Nat.succ_le_mono, H6. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series