def ud.no_lt_one

bend-osdev-u32@0.1.0.0 · PROOF_div.bend:50

import bend-osdev-u32@0.1.0.0/PROOF_div.bend as PROOFDiv

import Base

50def ud.no_lt_one(+np: Nat) -> {Nat.is_lt(1n+np, 1n) == True{} : Bool} -> Empty:
51  match np:
52    case 0n:
53      h => ud.bool_clash(h)
54    case 1n+q:
55      h => ud.bool_clash(h)

Uses (5)

Used by (2)