proposition: Lemma sig_forall_dec : {n | ~P n} + {forall n, P n}.
proof: Proof. assert (Hi: (forall n, 0 < INR n + 1)%R). { intros n. apply Rplus_le_lt_0_compat with (1 := (pos_INR n)); apply Rlt_0_1. } set (u n := (if HP n then 0 else / (INR n + 1))%R). assert (Bu: forall n, (u n <= 1)%R). { intros n. unfold u. case HP ; intros _. - apply Rle_0_1. - rewrite <- S_INR, <- Rinv_1. apply Rinv_le_contravar with (1 := Rlt_0_1). apply (le_INR 1); apply -> Nat.succ_le_mono; apply Nat.le_0_l. } set (E y := exists n, y = u n). destruct (completeness E) as [l [ub lub]]. - exists R1. intros y [n ->]. apply Bu. - exists (u O). now exists O. - assert (Hnp: forall n, not (P n) -> ((/ (INR n + 1) <= l)%R)). { intros n Hp. apply ub. exists n. unfold u. now destruct (HP n). } destruct (Rle_lt_dec l 0) as [Hl|Hl]. + right. intros n. destruct (HP n) as [H|H]. * exact H. * exfalso. apply Rle_not_lt with (1 := Hl). apply Rlt_le_trans with (/ (INR n + 1))%R. -- now apply Rinv_0_lt_compat. -- now apply Hnp. + left. set (N := Z.abs_nat (up (/l) - 2)). assert (H1l: (1 <= /l)%R). { rewrite <- Rinv_1. apply Rinv_le_contravar with (1 := Hl). apply lub. now intros y [m ->]. } assert (HN: (INR N + 1 = IZR (up (/ l)) - 1)%R). { unfold N. rewrite INR_IZR_INZ. rewrite inj_Zabs_nat. replace (IZR (up (/ l)) - 1)%R with (IZR (up (/ l) - 2) + 1)%R. - apply (f_equal (fun v => IZR v + 1)%R). apply Z.abs_eq. apply Zle_minus_le_0. apply (Zlt_le_succ 1). apply lt_IZR. apply Rle_lt_trans with (1 := H1l). apply archimed. - rewrite minus_IZR. simpl. ring. } assert (Hl': (/ (INR (S N) + 1) < l)%R). { rewrite <- (Rinv_inv l). apply Rinv_0_lt_contravar. { now apply Rinv_0_lt_compat. } rewrite S_INR. rewrite HN. ring_simplify. apply archimed. } exists N. intros H. apply Rle_not_lt with (2 := Hl'). apply lub. intros y [n ->]. unfold u. destruct (HP n) as [_|Hp]. * apply Rlt_le. now apply Rinv_0_lt_compat. * apply Rinv_le_contravar. -- apply Hi. -- apply Rplus_le_compat_r. apply le_INR. destruct (Nat.le_gt_cases n N) as [Hn|Hn]. 2: now apply Nat.le_succ_l. exfalso. destruct (proj1 (Nat.lt_eq_cases _ _) Hn) as [Hn'| ->]. 2: now apply Hp. apply Rlt_not_le with (2 := Hnp _ Hp). rewrite <- (Rinv_inv l). apply Rinv_0_lt_contravar. ++ apply Rplus_le_lt_0_compat. ** apply pos_INR. ** apply Rlt_0_1. ++ apply Rlt_le_trans with (INR N + 1)%R. ** apply Rplus_lt_compat_r. now apply lt_INR. ** rewrite HN. apply Rplus_le_reg_r with (-/l + 1)%R. ring_simplify. apply archimed. Qed.
imports: RIneq