proposition: Theorem rZltTrans : transitive rZ rZlt.
proof: Proof. red in |- *. intros x y z H' H'0; red in |- *; apply rltTrans with (y := valRz y); auto with stalmarck. Qed.
imports: Stalmarck(sTactic) Coq(Relation_Definitions) Coq(ZArith) Coq(Inverse_Image) Coq(Inclusion) Coq(Wf_nat) Coq(List)