proposition: Theorem samePolRzComp : forall p q : rZ, rZComp (samePolRz p q) = samePolRz p (rZComp q).
proof: Proof. intros p q; case p; case q; simpl in |- *; auto with stalmarck. Qed.
imports: Stalmarck(sTactic) Coq(Relation_Definitions) Coq(ZArith) Coq(Inverse_Image) Coq(Inclusion) Coq(Wf_nat) Coq(List)