def wn.not_lt_add

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

import Base

189# a + b < a never holds, nor s + b < b
190def wn.not_lt_add(a: Nat, b: Nat) -> {Nat.is_lt(Nat.add(a, b), a) == False{} : Bool}:
191  match a:
192    case 0n:
193      match b:
194        case 0n:
195          {==}
196        case 1n+q:
197          {==}
198    case 1n+p:
199      wn.not_lt_add(p, b)