m,a,a',b,b':
. (a = a' mod m) 
(b = b' mod m) ((a+b) = (a'+b') mod m)a,b1,b2:. a | b1 a | b2 a | b1+b2| Theorem | Name |
| m,a,a',b,b':. (a = a' mod m) (b = b' mod m) ((a+b) = (a'+b') mod m) | [add_functionality_wrt_eqmod] |
| cites the following: | |
| a,b1,b2:. a | b1 a | b2 a | b1+b2 | [divisor_of_sum] |