proposition: Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
proof: Proof. unfold lt, eq; intros ? ? LT ->; revert LT; apply Nat.lt_irrefl. Qed.
imports: OrderedType ZArith_base PeanoNat Peano_dec Compare_dec Ascii String NArith Ndec