proposition: Lemma pretty_N_go_step x s : (0 < x)%N → pretty_N_go x s = pretty_N_go (x `div` 10) (String (pretty_N_char (x `mod` 10)) s).
proof: Proof. unfold pretty_N_go; intros; destruct (wf_guard 32 N.lt_wf_0 x). destruct (wf_guard _ _). unfold pretty_N_go_help at 1; fold pretty_N_go_help. by destruct (decide (0 < x)%N); auto using pretty_N_go_help_irrel. Qed.
imports: stdpp(relations numbers) Coq(Ascii) stdpp(options)