proposition: Lemma not_wlt_len: forall (w1 w2:(list nat)) (a:nat), (length w2 <= length w1) -> not (wlt (cons (S a) w1) w2).
proof: Proof. induction w2. intros. intro. exfalso. apply (not_wlt_nil (cons (S a) w1)). assumption. intro. case a. intro. intro. apply IHw2 with (a:=a0). apply Nat.le_trans with (m:=(length (cons 0 w2))). simpl. auto with arith. assumption. apply wlt_w_0_inv. assumption. intros. intro. inversion H0. apply (Nat.lt_irrefl (length w1)). simpl in H. apply Nat.lt_trans with (m:=(length w2)); assumption. rewrite H4 in H. apply (Nat.nle_succ_diag_l (length w2)). assumption. rewrite H4 in H. apply (Nat.nle_succ_diag_l (length w2)). assumption. Qed.
imports: Arith Coq.Logic.Eqdep_dec Coq.Arith.Peano_dec List Recdef