Tidy proofs for pow256_slr and pow256_shr

[DavePearce]

See these comments from stackoverflow for suggestions on using calc.

UPDATE: I had a crack at this already, though didn't end up getting the desired result.

[DavePearce]

Ok, here's what I came up with:

def pow256_shr (n : Nat) (m : UInt8) (k : Nat) (p : n < 256^k) : (m.val * 256^k + n < 256^(k+1)) := by
  calc
    _ ≤ 255 * 256^k + n := by
              apply Nat.add_le_add_right
              apply Nat.mul_le_mul_right (256^k)
              exact Fin.is_le m.val
    _ < (255 + 1) * 256^k := by simp_arith; exact p
    _ = 256 * 256^k := by simp
    _ = 256^(k+1) := by exact Nat.pow_succ'.symm