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