proposition: Lemma pretty_N_go_ne_dash x s s' : s ≠ "-" +:+ s' → pretty_N_go x s ≠ "-" +:+ s'.
proof: Proof. revert s. induction (N.lt_wf_0 x) as [x _ IH]; intros s ?. assert (x = 0 ∨ 0 < x)%N as [->|?] by lia. - by rewrite pretty_N_go_0. - rewrite pretty_N_go_step by done. apply IH. { by apply N.div_lt. } unfold pretty_N_char. by repeat case_match. Qed.
imports: stdpp(relations numbers) Coq(Ascii) stdpp(options)