proposition: Lemma not_wlt_len_left : forall (w1 w2:(list nat)) (a:nat), (le (length w2) (length w1)) -> not (wlt (cons (S a) w1) w2).
proof: Proof. induction w2. intros. apply not_wlt_nil. intros. destruct a. intro. absurd (wlt (cons (S a0) w1) w2). apply IHw2. apply Nat.le_trans with (m:=(length (cons 0 w2))). auto with arith. assumption. apply wlt_w_0_inv. assumption. intro. inversion H0. assert (lt (length (cons (S a) w2)) (length w2)). apply Nat.le_lt_trans with (m := (length w1)); assumption. apply (not_lt_Sn_n (length w2)). assumption. rewrite H4 in H. apply (not_le_Sn_n (length w2)); assumption. rewrite H4 in H. apply (not_le_Sn_n (length w2)); assumption. Qed.
imports: Arith Coq.Logic.Eqdep_dec Coq.Arith.Peano_dec List Recdef