def AP.le_succ

bend-osdev-array@0.1.0.1 · PROOF.bend:70

import Base

70def AP.le_succ(y: Nat, x: Nat) -> {Nat.is_le(1n+y, x) == Nat.is_lt(y, x) : Bool}:
71  match y x:
72    case 0n 0n:
73      {==}
74    case 0n 1n+p:
75      match p:
76        case 0n:
77          {==}
78        case 1n+q:
79          {==}
80    case 1n+q 0n:
81      {==}
82    case 1n+q 1n+p:
83      AP.le_succ(q, p)