proposition: Theorem compare : forall c d : t, Compare lt eq c d.
proof: Proof. unfold lt, eq; intros; remember (N_of_ascii c ?= N_of_ascii d)%N as C; symmetry in HeqC; destruct C; [ apply EQ; replace c with (ascii_of_N (N_of_ascii c)) by apply ascii_N_embedding; replace d with (ascii_of_N (N_of_ascii d)) by apply ascii_N_embedding; f_equal; apply N.compare_eq | apply LT | apply GT; apply N.gt_lt]; assumption. Qed.
imports: OrderedType Bool Ascii NArith