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