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