proposition: Theorem lt_not_wf : ~ (well_founded lt).
proof: Proof. red; intro wf. case (not_decreasing _ lt). auto. exists f. exact f_decreases. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List