proposition: Lemma not_wlt_nil : forall (w:(list nat)), not (wlt w nil).
proof: Proof. induction w. intro. inversion H. case a. intro. inversion H. auto. intro. intro. inversion H. Qed.
imports: Arith Coq.Logic.Eqdep_dec Coq.Arith.Peano_dec List Recdef