proposition: Lemma pretty_N_go_ne_0 x s : s ≠ "0" → pretty_N_go x s ≠ "0".
proof: Proof. revert s. induction (N.lt_wf_0 x) as [x _ IH]; intros s ?. assert (x = 0 ∨ 0 < x < 10 ∨ 10 ≤ 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. } assert (x = 1 ∨ x = 2 ∨ x = 3 ∨ x = 4 ∨ x = 5 ∨ x = 6 ∨ x = 7 ∨ x = 8 ∨ x = 9)%N by lia; naive_solver. - rewrite 2!pretty_N_go_step by (try apply N.div_str_pos_iff; lia). apply IH; [|done]. trans (x `div` 10)%N; apply N.div_lt; auto using N.div_str_pos with lia. Qed.
imports: stdpp(relations numbers) Coq(Ascii) stdpp(options)