[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.