proposition: Theorem samePolRzRvlt : forall (p q : rZ) (r : rNat), rVlt p r -> rVlt (samePolRz q p) r.
proof: Proof. intros p q r; case q; auto with stalmarck. Qed.
imports: Stalmarck(sTactic) Coq(Relation_Definitions) Coq(ZArith) Coq(Inverse_Image) Coq(Inclusion) Coq(Wf_nat) Coq(List)