# [isabelle] mod_add1_eq - Theory Divides

Hello

`Just wondering if there is a problem with the lemma "mod_add1_eq"(see
``below) in the theory Divides.
`
(* Snippet from the divides theory which I am not able to verify*)
lemma mod_add1_eq: "(a+b) mod (c::nat) = (a mod c + b mod c) mod c"
apply (case_tac "c = 0", simp)
apply (blast intro: quorem_div_mod quorem_div_mod
quorem_add1_eq [THEN quorem_mod])
done
(* end of snippet *)

`Iam finding it a bit difficult to get this verified. Iam a new-comer
``both to Isabelle and to theorem verification, so if I have missed out on
``something really primitive, apologies for taking your time.
`

`Is there an easier way to verify "(a+b) mod (c::nat) = (a mod c + b mod
``c) mod c", though?
`
Regards
Srinivas

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