proposition: Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
proof: Proof. intros; intro. rewrite <- H0 in H; clear H0 y. unfold lt in H. exact (bits_lt_antirefl x H). Qed.
imports: OrderedType ZArith_base PeanoNat Peano_dec Compare_dec Ascii String NArith Ndec