law pl_le0_and

lawful-bytes@0.1.1.0 · proof_list.bend:73

import Base

73# 0 <= n, inside a conjunction.
74law pl_le0_and:
75  for +n: Nat
76  for +b: Bool
77  for +e: {b == True{} : Bool}
78  {(Nat.is_le(0n, n) && b) == True{} : Bool}