proposition: Lemma Acc_wlt_pad_ind : forall (n:nat), (forall (w:(list nat)), (lt (length w) (S n)) -> Acc wlt_pad w) -> forall (w:(list nat)), (length w)=(S n) -> Acc wlt_pad w.
proof: Proof. intros. elim (length_Sn_cons w n H0). intros a H1. elim H1. clear H1. intros w' H1. rewrite H1. rewrite H1 in H0. clear H1. generalize H0. pattern a, w'. apply AccElim2 with (RA:=lt) (RB:=wlt_pad). intros a' w'' H1 H2 H3. apply Acc_intro. intros w''' H4. inversion H4. elim (padd_len_lt_cons w1 (cons (S a0) w'')). intros w0 H9. rewrite H9. apply H1. rewrite <- H5. auto with arith. apply H. assert (lt (length (cons 0 w0)) (S (S n))). rewrite <- H9. rewrite padd_len_le_len. rewrite H5. rewrite H3. auto with arith. simpl. auto with arith. auto with arith. rewrite <- H9. rewrite padd_len_le_len. rewrite H5. assumption. simpl. auto with arith. simpl. auto with arith. apply H1. rewrite <- H5. auto with arith. apply H. rewrite H8. rewrite <- H3. auto with arith. simpl. rewrite H8. auto. apply H2. assumption. simpl. rewrite H8. auto. apply lt_wf. apply H. rewrite <- H0. auto with arith. Qed.
imports: Arith Coq.Logic.Eqdep_dec Coq.Arith.Peano_dec List Recdef