proposition: Theorem rnextRlt : forall m : rNat, rlt m (rnext m).
proof: Proof. intros m; unfold rlt, rnext in |- *. apply nat_of_P_lt_Lt_compare_complement_morphism. rewrite Pplus_one_succ_r; rewrite nat_of_P_plus_morphism; unfold nat_of_P in |- *; simpl in |- *; rewrite Nat.add_comm; simpl in |- *; auto with arith stalmarck. Qed.
imports: Stalmarck(sTactic) Coq(Relation_Definitions) Coq(ZArith) Coq(Inverse_Image) Coq(Inclusion) Coq(Wf_nat) Coq(List)