proposition: Lemma rltRmaxRight : forall n m : rNat, rlt m (rnext (rmax n m)).
proof: Proof. intros n m; unfold rmax in |- *; case (rltDec n m); auto with stalmarck; intros Rlt0. Casec Rlt0; intros Rlt0; auto with stalmarck. apply rltTrans with (y := n); auto with stalmarck. rewrite <- Rlt0; auto with stalmarck. Qed.
imports: Stalmarck(sTactic) Coq(Relation_Definitions) Coq(ZArith) Coq(Inverse_Image) Coq(Inclusion) Coq(Wf_nat) Coq(List)