proposition: Lemma rnextMono : forall m n : rNat, rlt m n -> rlt (rnext m) (rnext n).
proof: Proof. intros m n H'. case (rltDec (rnext m) n); intros Rlt0; auto with stalmarck. apply rltTrans with (y := n); auto with stalmarck. case Rlt0; intros Rlt1. elim (rNextInv n m); auto with stalmarck; intros Rlt2; absurd (rlt m m); auto with stalmarck. rewrite Rlt2 in H'; auto with stalmarck. apply rltTrans with (y := n); auto with stalmarck. rewrite <- Rlt1; auto with stalmarck. Qed.
imports: Stalmarck(sTactic) Coq(Relation_Definitions) Coq(ZArith) Coq(Inverse_Image) Coq(Inclusion) Coq(Wf_nat) Coq(List)