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