# [PVS-Help] Re: using modulo_arithmetic

```"R. Colvin" <robert@itee.uq.edu.au> wrote:
> Hi, I'm having trouble proving the following theorem using the
> modulo_arithmetic theory.
>
> 	modding: THEOREM (forall (b: posnat), (x: nat):
> 		rem(b+1)(x + b) =
> 			if rem(b+1)(x) = 0 then
> 				b
> 			else
> 				rem(b+1)(x) - 1 endif)
>
> I've simplified it to some extent but seem to be overlooking the
> crucial property/technique for 'rem' that would allow me to complete
> the proof.  Does anyone have a tip on how to proceed?

This is more roundabout than I would like, but does the trick with PVS
3.1:

(""
(grind)
(("1"
(lemma "commutative_add" ("x" "b!1" "y" "x!1"))
(replace -1)
(use "rem_sum_assoc")
(assert))
("2"
(lemma "same_remainder"
("b" "1 + b!1" "x" "b!1 + x!1" "y" "x!1 - 1"))
(assert)
(use "divides_reflexive")
(assert)
(replace -2)
(lemma "rem_sum_assoc" ("b" "1 + b!1" "x" "x!1 - 1" "n" "1"))
(assert)
(lemma "rem_add_one" ("b" "1 + b!1" "x" "x!1 - 1"))
(assert))))

Regards,
--
Jerry James
http://www.ittc.ku.edu/~james/

```