Re: [isabelle] cardinality

I suggest you begin by proving the lemma "x ~= y ==> card({x,y})=2", which is trivial. Then you get rid of card and merely have to exhibit x and y.

Larry Paulson

On 14 Mar 2006, at 16:25, kuecuek at wrote:

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 ??

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