law pl_r_step_le

lawful-bytes@0.1.1.0 · proof_list.bend:98

import Base

98law pl_r_step_le:
99  for +z: Bool
100  for +r: Nat
101  for +p: Nat
102  for +h: {Nat.is_le(r, p) == True{} : Bool}
103  {Nat.is_le(Bool.pick(Nat, z, 0n, 1n+r), 1n+p) == True{} : Bool}