ch6_divergence_to_infinity.mv

# Real-valued sequences
<hint title="📦 Import libraries (click to open/close)">
```coq
Set Default Goal Selector "!".

Require Import Stdlib.Reals.Reals.
Require Import Waterproof.Tactics.
Require Import Waterproof.Notations.Common.
Require Import Waterproof.Notations.Reals.
Require Import Waterproof.Notations.Sets.
Require Import Waterproof.Chains.
Require Import Waterproof.Automation.
Require Import Waterproof.Libs.Analysis.Sequences.

Require Import Waterproof.Libs.Reals.

Waterproof Enable Automation RealsAndIntegers.
Waterproof Enable Automation Intuition.

Open Scope R_scope.
Open Scope subset_scope.

Definition prop_5_2_2 := is_bounded_equivalence.
Definition application_of_prop_5_2_2 (a : ℕ → ℝ) :=
  iff_trans(_, _, (is_bounded_above a ∧ is_bounded_below a), prop_5_2_2 a).

Notation "'max' ( x , y )" := (Nat.max x y)
  (format "max '(' x ,  y ')'") : nat_scope.
Notation "'min' ( x , y )" := (Nat.min x y)
  (format "min '(' x ,  y ')'") : nat_scope.

Notation "'max' ( x , y )" := (Rmax x y)
  (format "max '(' x ,  y ')'") : R_scope.
Notation "'min' ( x , y )" := (Rmin x y)
  (format "min '(' x ,  y ')'") : R_scope.

Inductive answer : Type :=
| Yes : answer.

Set Bullet Behavior "Waterproof Relaxed Subproofs".
```
</hint>
## Exercise 6.8.2 (Proposition 6.6.2 item (i))
```coq
Section Prop_6_2_2_i.
Variable a : ℕ → ℝ.
Definition a_opp (n : ℕ) := - a(n).
```

```coq
Lemma exercise_6_8_2 :
  a _diverges to ∞_
    ⇔
  a_opp _diverges to -∞_.
Proof.
```
<input-area>
```coq

```
</input-area>
```coq
Qed.

End Prop_6_2_2_i.
```

## Declaration of own work

Please declare that the work above is your own work, by writing `Yes.` as an answer on the line below. In particular, this means that the proofs above are typed by yourself, and that you could give an explanation of the proof when asked.
```coq
Definition own_work : answer. exact
```
<input-area>
```coq

```
</input-area>
```coq
Qed.
```