proposition: Lemma lt_inv_le : forall a n b a' n' b', cons a n b < cons a' n' b' -> a <= a'.
proof: Proof. intros a n b a' n' b' H. case (lt_inv H). auto with T1. intros [(e,i)|(e,(e',i))]. subst a; auto with T1. subst a; auto with T1. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List