proposition: Lemma lex_natxnat_snd : forall (x y1 y2:nat), (lt y1 y2) -> (lex_natxnat (x,y1) (x,y2)).
proof: Proof. intros. unfold lex_natxnat. unfold make_mwlt. simpl. apply wlt_wlt_gen. auto. apply wlt_lt_gen; auto. Qed.
imports: Arith Coq.Logic.Eqdep_dec Coq.Arith.Peano_dec List Recdef