proposition: Lemma rmaxRlt : forall n m p : rNat, rlt m n -> rlt p n -> rlt (rmax m p) n.
proof: Proof. intros n m p; unfold rmax in |- *; case (rltDec m p); auto with stalmarck. Qed.
imports: Stalmarck(sTactic) Coq(Relation_Definitions) Coq(ZArith) Coq(Inverse_Image) Coq(Inclusion) Coq(Wf_nat) Coq(List)