def nat.le_succ

bend-osdev-algo@0.1.0.0 · PROOF.bend:98

import bend-osdev-algo@0.1.0.0/PROOF.bend as PROOF

import Base

98def nat.le_succ(a: Nat, b: Nat, e: {Nat.is_le(a, b) == True{} : Bool}) -> {Nat.is_le(a, 1n+b) == True{} : Bool}:
99  match a b:
100    case 0n _:
101      {==}
102    case 1n+ap 0n:
103      Empty.absurd({Nat.is_le(1n+ap, 1n) == True{} : Bool}, absurd.ft(e))
104    case 1n+ap 1n+bp:
105      nat.le_succ(ap, bp, e)

Uses (5)

Used by (2)