def nat.lt_irrefl

bend-osdev-algo@0.1.0.0 · PROOF.bend:84

import bend-osdev-algo@0.1.0.0/PROOF.bend as PROOF

import Base

84def nat.lt_irrefl(x: Nat) -> {Nat.is_lt(x, x) == False{} : Bool}:
85  match x:
86    case 0n:
87      {==}
88    case 1n+p:
89      nat.lt_irrefl(p)

Uses (3)

Used by (1)

bend-osdev-algo@0.1.0.0/PROOF:bitseq.next_hit