[isabelle] mod_mult_distrib

Hi all!

I want to prove mod_mult_distrib: "(a*b) mod (c::int)= ((a mod c) * (b mod c)) mod c". A similar property is already proved for a, b c natural numbers. I will like to have it for positive, nonzero integers. 
Can someone give me an idea how to prove it? (maybe by using the property for nat)

Thank you, Stefania Barzan


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