theorem znsubpos (m n: nat): $ n <= m -> m -ZN n = b0 (m - n) $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | lenlt | n <= m <-> ~m < n |
|
2 | ifneg | ~m < n -> if (m < n) (b1 (n - suc m)) (b0 (m - n)) = b0 (m - n) |
|
3 | 2 | conv znsub | ~m < n -> m -ZN n = b0 (m - n) |
4 | 1, 3 | sylbi | n <= m -> m -ZN n = b0 (m - n) |