proposition: Lemma pretty_N_char_inj x y : (x < 10)%N → (y < 10)%N → pretty_N_char x = pretty_N_char y → x = y.
proof: Proof. compute; intros. by repeat (discriminate || case_match). Qed.
imports: stdpp(relations numbers) Coq(Ascii) stdpp(options)