proposition: Theorem lt_not_gt : forall a b, a < b -> ~ b < a.
proof: Proof. intros o1 o2 H H0. generalize (lt_trans H H0). intro H2; case (lt_irr H2). Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List