[isabelle] need help



hallo,

i try to solve an equation but it is realy complex can anybody help me?
if i try with numbers then i can show it with "auto" but if i use variables 
then i can not proof it.


the equations below are given 

y1 ^2 = x1 ^3 + a*x1 + b
y2 ^2 = x2 ^ 3 + a*x2 + b

and 

x3 =  ((((y1 - y2) *  ((x1 - x2) ^ nat (p -2 ))) mod p) ^ 2 - x1 - x2) mod p
y3 = ((((y1 - y2) *  ((x1 - x2) ^ nat (p -2 ))) mod p) * (x1 - x3) - y1) mod p


and i must to show that y3^2 = x3^3 + a*x3 + b

if you put the definitionof y3 and x3 in last equation you would see how 
complex it is :(

can anybody give a trick to proof something like that?

thanks a lot





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