law le_shift

lawful-bytes@0.1.1.0 · proof_append.bend:129

import Base

129law le_shift:
130  for +a: Nat
131  for +k: Nat
132  for +m: Nat
133  for +h: {Nat.is_le(Nat.add(a, 1n+k), m) == True{} : Bool}
134  {Nat.is_le(Nat.add(Nat.add(a, 1n), k), m) == True{} : Bool}