proposition: Lemma cmp_correct : correct nat lt cmp.
proof: Proof. red. induction x;destruct y;simpl;try constructor;auto with arith. destruct (IHx y). subst y;constructor;trivial. constructor;auto with arith. constructor;auto with arith. Qed.
imports: Arith RelationClasses