proposition: Theorem rZEvalCompInv : forall (a : rZ) (f : rNat -> bool), rZEval f (rZComp a) = negb (rZEval f a).
proof: Proof. intros a f; case a; simpl in |- *; auto with stalmarck. intros r; case (f r); auto with stalmarck. Qed.
imports: Coq(List)