proposition: Lemma wlt_zs_wlt_right : forall (n:nat) (w1 w2:(list nat)), (wlt w1 (app (zs n) w2)) -> (wlt w1 w2).
proof: Proof. induction n. auto. simpl. intros. apply IHn. apply wlt_w_0_inv. assumption. Qed.
imports: Arith Coq.Logic.Eqdep_dec Coq.Arith.Peano_dec List Recdef