proposition: Lemma wlt_lt_gen : forall (a1 a2:nat) (w1 w2:list nat), (length w1) = (length w2) -> (lt a1 a2) -> (wlt (cons a1 w1) (cons a2 w2)).
proof: Proof. intros. destruct a2. exfalso. apply (Nat.nlt_0_r a1). assumption. destruct a1. apply wlt_0_w. apply wlt_len_gen. rewrite H. auto with arith. apply wlt_lt; auto with arith. Qed.
imports: Arith Coq.Logic.Eqdep_dec Coq.Arith.Peano_dec List Recdef