proposition: Lemma rNextS : forall n : rNat, nat_of_P (rnext n) = S (nat_of_P n).
proof: Proof. intros n; unfold rnext, nat_of_P in |- *; simpl in |- *. rewrite Pmult_nat_succ_morphism; auto with stalmarck. Qed.
imports: Stalmarck(sTactic) Coq(Relation_Definitions) Coq(ZArith) Coq(Inverse_Image) Coq(Inclusion) Coq(Wf_nat) Coq(List)