def un.le_succ_self

bend-osdev-u32@0.1.0.0 · PROOF.bend:212

import Base

212def un.le_succ_self(x: Nat) -> {Nat.is_le(x, 1n+x) == True{} : Bool}:
213  match x:
214    case 0n:
215      {==}
216    case 1n+p:
217      un.le_succ_self(p)