proposition: Lemma rltRnext2Inv : forall n m : rNat, rlt (rnext n) (rnext m) -> rlt n m.
proof: Proof. intros n m H'; case (rNextInv (rnext n) m); auto with stalmarck. intros H'0; rewrite <- H'0; auto with stalmarck. intros H'1; apply rltTrans with (y := rnext n); auto with stalmarck. Qed.
imports: Stalmarck(sTactic) Coq(Relation_Definitions) Coq(ZArith) Coq(Inverse_Image) Coq(Inclusion) Coq(Wf_nat) Coq(List)