Fix potential stack overflow related to `Pretty N`.

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.

tests/pretty.v

 From stdpp Require Import pretty.
+From Coq Require Import Ascii.
 
 Section N.
   Local Open Scope N_scope.
@@ -17,6 +18,17 @@ Section N.
   Proof. reflexivity. Qed.
 End N.
 
+(** Minimized version of:
+
+  https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Stack.20overflow.20in.20Qed.2E
+
+Fixed by making the [wp_guard] in [pretty_N_go] proportional to the
+size of the input so that it blocks in case the input is an open term. *)
+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. Qed.
+
 Section nat.
   Local Open Scope nat_scope.