def un.le_succ

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

import Base

123def un.le_succ(y: Nat, x: Nat) -> {Nat.is_le(1n+y, x) == Nat.is_lt(y, x) : Bool}:
124  match y x:
125    case 0n 0n:
126      {==}
127    case 0n 1n+p:
128      match p:
129        case 0n:
130          {==}
131        case 1n+q:
132          {==}
133    case 1n+q 0n:
134      {==}
135    case 1n+q 1n+p:
136      un.le_succ(q, p)