def lt_irrefl

bend-collections-laws-math@1.0.0.0 · proofs/lib/nat.bend:51

import Base

51def lt_irrefl(+n: Nat) -> {Nat.is_lt(n, n) == False{} : Bool}:
52  match n:
53    case 0n:
54      {==}
55    case 1n+p:
56      lt_irrefl(p)