proposition: Theorem rnextNotZero : forall m : rNat, rlt zero (rnext m).
proof: Proof. intros m; unfold nat_of_P, rnext, rlt in |- *; elim m; simpl in |- *; auto with stalmarck. Qed.
imports: Stalmarck(sTactic) Coq(Relation_Definitions) Coq(ZArith) Coq(Inverse_Image) Coq(Inclusion) Coq(Wf_nat) Coq(List)