def gt.lt_self

bend-osdev-gf@0.1.1.0 · proof_tab.bend:133

import bend-osdev-gf@0.1.1.0/proof_tab.bend as ProofTab

import Base

133def gt.lt_self(+x: Nat) -> {Nat.is_lt(x, 1n+x) == True{} : Bool}:
134  match x:
135    case 0n:
136      {==}
137    case 1n+p:
138      gt.lt_self(p)

Uses (3)

Used by (1)

bend-osdev-gf@0.1.1.0/proof_tab:gt.lt_self_add