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