proposition: Lemma lt_not_le: forall a b, a < b -> ~ b <= a.
proof: Proof. red; unfold le. intros a b H H0; case H0;intro. subst b; absurd (lt a a);auto with T1. absurd (lt a a); eauto with T1. eapply lt_trans;eauto. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List