proposition: Lemma wlt_w_0_inv: forall (w1 w2:(list nat)), (wlt w1 (cons 0 w2)) -> (wlt w1 w2).
proof: Proof. induction w1. intros. inversion H. assumption. intros. inversion H. apply wlt_0_w. auto. assumption. Qed.
imports: Arith Coq.Logic.Eqdep_dec Coq.Arith.Peano_dec List Recdef