fact: Definition compare (a b : ascii) : Compare lt eq a b := match cmp a b as z return _ = z -> _ with | Lt => fun E => LT E | Gt => fun E => GT (compare_helper_gt E) | Eq => fun E => EQ (compare_helper_eq E) end Logic.eq_refl.
imports: OrderedType ZArith_base PeanoNat Peano_dec Compare_dec Ascii String NArith Ndec