law to_nat_shrn_lt.m

lawful-words@0.1.0.0 · proof_u32.bend:1131

import Base

1131law to_nat_shrn_lt.m:
1132  for +a: U32
1133  for +k: Nat
1134  for +m: Nat
1135  for +hm: {Nat.pow(2n, 32n) == m : Nat}
1136  {Nat.is_lt(U32.to_nat(U32.shrn(a, k)), Nat.pow(2n, Nat.sub(32n, k))) == True{} : Bool}