proposition: Theorem rNextInv : forall n m : rNat, rlt n (rnext m) -> n = m \/ rlt n m.
proof: Proof. intros n m H'. generalize (nat_of_P_lt_Lt_compare_morphism _ _ H'). rewrite rNextS. intros H'0; case (proj1 (Nat.lt_eq_cases _ _) (proj1 (Nat.lt_succ_r _ _) H'0)). intros H'1; right; red in |- *; apply nat_of_P_lt_Lt_compare_complement_morphism; auto with stalmarck. intros H'1; left; apply nat_of_P_inj; auto with stalmarck. Qed.
imports: Stalmarck(sTactic) Coq(Relation_Definitions) Coq(ZArith) Coq(Inverse_Image) Coq(Inclusion) Coq(Wf_nat) Coq(List)