proposition: Lemma not_wlt_Sn_0 : forall (w1 w2:(list nat)) (a:nat), (length w1) = (length w2) -> not (wlt (cons (S a) w1) (cons 0 w2)).
proof: Proof. intros. intro. inversion H0. apply (not_wlt_len_left w1 w2 a). rewrite H. auto with arith. apply wlt_w_0_inv. assumption. Qed.
imports: Arith Coq.Logic.Eqdep_dec Coq.Arith.Peano_dec List Recdef