# [isabelle] cardinality

hallo again
i have still problem with cardinality :( maybe can anyone help me
i want to show that
If p is an odd prime and a is a "Quadratischer rest" in p (EX x. [x^2 = a]
(mod p)) then there are exactly two square roots modulo p.
these are in this fall -x and x.
but i can not prove that in isabelle.
lemma "[|zprime p; 2<p; ~[a=0](mod p); QuadRes p a|] ==>
card {(x::int).[x^2 = a] (mod p)}=(2::nat)"
is it right?
i have tried to show with the help of the lemma zcong_square_zless:
[| zprime p; 0 < a; a < p; [a * a = 1] (mod p) |] ==> a = 1 | a = p - 1
in this case i formula my lemma
lemma "[| zprime p;2<p; 0 < a; a < p; [a * a = 1] (mod p) |]
==> card {(a::int).[a * a = 1] (mod p) }=(2::nat)"
but i couldn't prove it again.
can anybody give an idea ??
thanks
best regards

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*