law le_antisym

lawful-bytes@0.1.1.0 · proof_fast_append.bend:250

import Base

250law le_antisym:
251  for +a: Nat
252  for +b: Nat
253  for +h1: {Nat.is_le(a, b) == True{} : Bool}
254  for +h2: {Nat.is_le(b, a) == True{} : Bool}
255  {a == b : Nat}