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