proposition: Theorem lt_neq : forall x y : nat, x < y -> x <> y.
proof: Proof. unfold not in |- *; intros x y H H1; elim (Nat.lt_irrefl x); pattern x at 2 in |- *; rewrite H1; auto. Qed.
imports: Coq(ArithRing) Coq(Compare_dec) Coq(Wf_nat) Coq(Arith) Coq(Lia)