[isabelle] need help by mod

Hallo everybody

i have some problems with modulo and power :(

i need following prooofs but i couldn't show these. 

1) ((a::int) - b) mod p = (a mod p - b mod p) mod p 
there is a lemma called zmod_zadd1_eq in IntDiv. i have tried to use this 
lemma with the variable "-b" but it doesn't help.

2)"(a::int) mod p = b mod p ==> a ^ k mod p = b ^ k mod p"
by this lemma i have problems too.

could anyone help me?

thanks for your helps

best regards

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