theorem shr12 (a: nat): $ shr a 1 = a // 2 $;
2 ^ 1 = 2 -> a // 2 ^ 1 = a // 2
2 ^ 1 = 2 -> shr a 1 = a // 2
2 ^ 1 = 2
shr a 1 = a // 2