proposition: Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
proof: Proof. intros x y H. contradict H. rewrite H. apply Pos.lt_irrefl. Qed.
imports: OrderedType ZArith_base PeanoNat Peano_dec Compare_dec Ascii String NArith Ndec