proposition: Lemma pretty_N_go_help_irrel x acc1 acc2 s : pretty_N_go_help x acc1 s = pretty_N_go_help x acc2 s.
proof: Proof. revert x acc1 acc2 s; fix FIX 2; intros x [acc1] [acc2] s; simpl. destruct (decide (0 < x)%N); auto. Qed.
imports: stdpp(relations numbers) Coq(Ascii) stdpp(options)