proposition: Theorem lt_not_eq : forall c d : ascii, lt c d -> ~ eq c d.
proof: Proof. unfold lt, eq; red; intros; assert (N_of_ascii c = N_of_ascii d) as eq' by (f_equal; assumption); generalize dependent eq'; apply N.lt_neq; assumption. Qed.
imports: OrderedType Bool Ascii NArith