def wn.le_succ

bend-osdev-word64@0.1.1.0 · proof_value.bend:107

import Base

107def wn.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      wn.le_succ(q, p)