law le_antisym

lawful-fields@0.1.1.0 · proof_cut.bend:55

import Base

55law le_antisym:
56  for +a: Nat
57  for +b: Nat
58  for +h1: {Nat.is_le(a, b) == True{} : Bool}
59  for +h2: {Nat.is_le(b, a) == True{} : Bool}
60  {a == b : Nat}