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