proposition: Theorem rZCompEq : forall a b : rZ, rZComp a = rZComp b -> a = b.
proof: Proof. intros a b; case a; case b; simpl in |- *; auto with stalmarck; intros a' b' H; inversion H; auto with stalmarck. Qed.
imports: Stalmarck(sTactic) Coq(Relation_Definitions) Coq(ZArith) Coq(Inverse_Image) Coq(Inclusion) Coq(Wf_nat) Coq(List)