proposition: Lemma nat_of_ascii_injective : forall a b, nat_of_ascii a = nat_of_ascii b <-> a = b.
proof: Proof. intros a b; split; intro H; [ apply (f_equal ascii_of_nat) in H; repeat rewrite ascii_nat_embedding in H | apply (f_equal nat_of_ascii) in H ]; trivial. Qed.
imports: Coq.ZArith.ZArith Coq.Strings.String Coq.Strings.Ascii Coq.Structures.OrderedType Fiat.Common.Coq__8_4__8_5__Compat