proposition: Lemma wlt_wlt_pad : forall (w1 w2:(list nat)), (length w1) = (length w2) -> (wlt w1 w2) -> (wlt_pad w1 w2).
proof: Proof. intros w1 w2. generalize w1. clear w1. induction w2. intros. exfalso. apply (not_wlt_nil w1). assumption. destruct w1. intros. discriminate H. intros. inversion H0. destruct a. apply wlt_pad_wlt_pad. auto. apply IHw2. auto. apply wlt_w_0_inv. assumption. rewrite <- (padd_cons_0 w1 w2 a). apply wlt_pad_len. injection H. intro. rewrite H5. auto with arith. auto. destruct n. apply wlt_pad_wlt_pad. auto with arith. apply IHw2. auto with arith. apply wlt_w_0_inv. apply wlt_0_w_inv. rewrite <- H1 in H0. assumption. exfalso. apply (not_wlt_Sn_0 w1 w2 n). auto with arith. rewrite <- H1 in H0. assumption. exfalso. apply (Nat.lt_irrefl (length w2)). injection H. intro. rewrite H6 in H2. assumption. apply wlt_pad_lt. auto with arith. assumption. apply wlt_pad_wlt_pad. auto with arith. apply IHw2. auto with arith. assumption. Qed.
imports: Arith Coq.Logic.Eqdep_dec Coq.Arith.Peano_dec List Recdef