proposition: Lemma rlex_nat3_1 : forall (y z m : nat), (rlex_nat3 (0, y, z) (0, m, S z)).
proof: Proof. intros. unfold rlex_nat3. unfold make_mwlt. destruct z. simpl. apply wlt_nil. simpl. apply wlt_lt; auto with arith. Qed.
imports: Arith Coq.Logic.Eqdep_dec Coq.Arith.Peano_dec List Recdef