fact: Definition rZComp (r : rZ) : rZ := match r with | rZPlus m => rZMinus m | rZMinus m => rZPlus m end.
imports: Stalmarck(sTactic) Coq(Relation_Definitions) Coq(ZArith) Coq(Inverse_Image) Coq(Inclusion) Coq(Wf_nat) Coq(List)