theorem modmod (a m n: nat): $ m || n -> a % n % m = a % m $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | id | m || n -> m || n |
|
| 2 | eqmmod | mod(n): a % n = a |
|
| 3 | 2 | a1i | m || n -> mod(n): a % n = a |
| 4 | 1, 3 | dvdeqm | m || n -> mod(m): a % n = a |
| 5 | 4 | conv eqm | m || n -> a % n % m = a % m |