proposition: Theorem samePolRzInvRvlt : forall (p q : rZ) (r : rNat), rVlt (samePolRz q p) r -> rVlt p r.
proof: Proof. intros p q r; case q; simpl in |- *; auto with stalmarck. intros H' H'0; replace p with (rZComp (rZComp p)); auto with stalmarck. Qed.
imports: Stalmarck(sTactic) Coq(Relation_Definitions) Coq(ZArith) Coq(Inverse_Image) Coq(Inclusion) Coq(Wf_nat) Coq(List)