law le_antisym

lawful-bytes@0.1.1.0 · proof_fast_find.bend:801

import Base

801law le_antisym:
802  for +a: Nat
803  for +b: Nat
804  for +h1: {Nat.is_le(a, b) == True{} : Bool}
805  for +h2: {Nat.is_le(b, a) == True{} : Bool}
806  {a == b : Nat}