Consider this theorem:

```
Theorem f3x: forall (f: bool -> bool) b, f (f (f b)) = f b.
```

*(It is an exercise from a popular book, but I would like not to make it easily searchable, as per the request of the authors, so the name is altered. What follows is my own work.)*

It can be proven with the tactic of brutality:

```
Proof.
intros. destruct (f true) eqn: T, (f false) eqn: F, b.
* rewrite T, T, T. reflexivity.
* rewrite F, T, T. reflexivity.
* rewrite T, T, T. reflexivity.
* rewrite F, F, F. reflexivity.
* rewrite T, F, T. reflexivity.
* rewrite F, T, F. reflexivity.
* rewrite T, F, F. reflexivity.
* rewrite F, F, F. reflexivity.
Qed.
```

â€” So it must be true. Giving it some informal thought, there are 2 kinds of subsets in the domain of a function: attractors and cycles. With `bool`

, it is trivial: there is one function with a 2-cycle *( negb)*, one function with 2 attractors

*(*and two functions with one attractor

`id`

)*(*.

`const true`

and `const false`

)It is therefore plausible to believe that these two lemmas describe the situation with fidelity:

```
Lemma bool_attractor:
forall f (b: bool),
f (f b) = f b -> f (f (f b)) = f b.
Lemma bool_cycle:
forall f (b: bool),
f (f b) <> f b -> f (f (f b)) = f b.
```

For the first one, the proof is immediate:

```
Proof. intros. rewrite H, H. reflexivity. Qed.
```

â€” But I was unable to prove the latter. *(Other than by reference to f3x.)* Once I

`intro`

the boolean value, the hypothesis specializes to it, and I can never prove both `f true = false`

and `f false = true`

. The inequality sign does not help, since I do not really know how to either transform it to equality or utilize directly, so I resort to converting it with a lemma like `b <> b' -> b = negb b' /\ negb b = b'`

, or otherwise rephrase the problem in terms of `negb`

.Please explain this situation to me. Should I think that the kind of reasoning I am trying to apply here is too *Â«classicalÂ»* for Coq? Or am I missing some sharp move?