proposition: Lemma ex_lim_seq_geom_m (q : R) : q <= -1 -> ~ ex_lim_seq (fun n => q ^ n).
proof: Proof. intros Hq [l H]. apply is_lim_seq_spec in H. destruct l as [l| |]. case: Hq => Hq. case: (H (mkposreal _ Rlt_0_1)) => /= {H} N H. move: (fun n Hn => Rabs_lt_between_Rmax _ _ _ (proj1 (Rabs_lt_between' _ _ _) (H n Hn))). set M := Rmax (l + 1) (- (l - 1)) => H0. case: (fun Hq => Pow_x_infinity q Hq M) => [ | N0 H1]. rewrite Rabs_left. apply Ropp_lt_cancel ; by rewrite Ropp_involutive. apply Rlt_trans with (1 := Hq) ; apply Ropp_lt_cancel ; rewrite Ropp_involutive Ropp_0 ; by apply Rlt_0_1. move: (H0 _ (Nat.le_add_r N N0)). by apply Rle_not_lt, Rge_le, H1, MyNat.le_add_l. case: (H (mkposreal _ Rlt_0_1)) => /= {H} N H. rewrite Hq in H => {q Hq}. move: (H _ (le_n_2n _)) ; rewrite pow_1_even ; case/Rabs_lt_between' => _ H1. have H2 : (N <= S (2 * N))%nat. by apply Nat.le_trans with (1 := le_n_2n _), Nat.le_succ_diag_r. move: (H _ H2) ; rewrite pow_1_odd ; case/Rabs_lt_between' => {H} H2 _. move: H1 ; apply Rle_not_lt, Rlt_le. pattern 1 at 2 ; replace (1) with ((-1)+2) by ring. replace (l+1) with ((l-1)+2) by ring. by apply Rplus_lt_compat_r. case: (H 0) => {H} N H. have H0 : (N <= S (2 * N))%nat. by apply Nat.le_trans with (1 := le_n_2n _), Nat.le_succ_diag_r. move: (H _ H0) ; apply Rle_not_lt ; rewrite /pow -/pow. apply Rmult_le_0_r. apply Rle_trans with (1 := Hq), Ropp_le_cancel ; rewrite Ropp_involutive Ropp_0 ; by apply Rle_0_1. apply Ropp_le_contravar in Hq ; rewrite Ropp_involutive in Hq. rewrite pow_sqr -Rmult_opp_opp ; apply pow_le, Rmult_le_pos ; apply Rle_trans with (2 := Hq), Rle_0_1. case: (H 0) => {H} N H. move: (H _ (le_n_2n _)). apply Rle_not_lt. apply Ropp_le_contravar in Hq ; rewrite Ropp_involutive in Hq. rewrite pow_sqr -Rmult_opp_opp ; apply pow_le, Rmult_le_pos ; apply Rle_trans with (2 := Hq), Rle_0_1. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Lub Markov Hierarchy