As reported by @simongregersen at https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Stack.20overflow.20in.20Qed.2E, lemmas involving `Pretty N`

could lead to stack overflow. I minimized his problem as follows:

```
Lemma test_no_stack_overflow p n :
get n (pretty (N.pos p)) ≠ Some "_"%char →
get (S n) ("-" +:+ pretty (N.pos p)) ≠ Some "_"%char.
Proof. intros Hlem. apply Hlem. (* stack overflow *) Qed.
```

The problem is that Coq's conversion unfolds too much, and triggers the `wf_guard 32`

in:

```
Definition pretty_N_go (x : N) : string → string :=
pretty_N_go_help x (wf_guard 32 N.lt_wf_0 x).
```

The `wf_guard`

is needed to make sure that computation of `pretty n`

for concrete numbers `n`

works (see tests in `tests/pretty.v`

). However, due to concrete number 32, which adds `2 ^ n`

`Acc_intro`

constructors to the opaque accessibility proof `N.lt_wf_0`

for the well-founded recursion, Coq's conversion might unfold `wf_guard 32`

too eagerly.

I hence changed the `32`

into `S (N.size_nat x)`

, which causes the tests in `tests/pretty.v`

to still work, and the stack overflow to disappear. The key idea is that `S (N.size_nat x)`

is not a concrete number if `x`

is an open term, thus preventing `wf_guard`

from unfolding.