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