proposition: Theorem lt_irr : forall a, ~ a < a.
proof: Proof. induction a. red;inversion_clear 1. intro H; case (lt_inv H); intuition. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List