theorem shrshlid (a b: nat): $ shr (shl a b) b = a $;
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | muldiv1 | 2 ^ b != 0 -> a * 2 ^ b // 2 ^ b = a |
|
2 | 1 | conv shl, shr | 2 ^ b != 0 -> shr (shl a b) b = a |
3 | pow2ne0 | 2 ^ b != 0 |
|
4 | 2, 3 | ax_mp | shr (shl a b) b = a |