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