proposition: Lemma wlt_wlt_pad_zs : forall (w1 w2:(list nat)), (length w1) < (length w2) -> (wlt w1 w2) -> (wlt_pad (padd w1 w2) w2).
proof: Proof. intros. apply wlt_wlt_pad. apply padd_len_le_len. auto with arith. apply wlt_wlt_zs_left. assumption. Qed.
imports: Arith Coq.Logic.Eqdep_dec Coq.Arith.Peano_dec List Recdef