proposition: Lemma tail_lt_cons : forall b n a, nf (cons a n b)-> b < cons a n b.
proof: Proof. induction b. constructor. constructor 2. inversion H;auto. Qed.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List