def uq.le_succ

bend-osdev-algo@0.1.0.0 · proof_u32.bend:107

import Base

107def uq.le_succ(y: Nat, x: Nat) -> {Nat.is_le(1n+y, x) == Nat.is_lt(y, x) : Bool}:
108  match y x:
109    case 0n 0n:
110      {==}
111    case 0n 1n+p:
112      match p:
113        case 0n:
114          {==}
115        case 1n+q:
116          {==}
117    case 1n+q 0n:
118      {==}
119    case 1n+q 1n+p:
120      uq.le_succ(q, p)