Nuprl - Pf modulus

1. a:
2. n:
3. a < 0

if ((-a) rem n)=0 0 else n-((-a) rem n) fi

By: Analyze

Generated subgoals:

1 if ((-a) rem n)=0 0 else n-((-a) rem n) fi

2 0if ((-a) rem n)=0 0 else n-((-a) rem n) fi

About:

1	`if ((-a) rem n)=0 0 else n-((-a) rem n) fi`
2	`0if ((-a) rem n)=0 0 else n-((-a) rem n) fi`