def lt_succ_le_succ

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/nat.bend:134

import Base

134def lt_succ_le_succ(+a: Nat, +b: Nat, e: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_le(1n+a, b) == True{} : Bool}:
135  match a b:
136    case _ 0n:
137      Empty.absurd({Nat.is_le(1n+a, 0n) == True{} : Bool}, lt_zero_absurd(a, e))
138    case 0n 1n+q:
139      zero_le(q)
140    case 1n+p 1n+q:
141      lt_succ_le_succ(p, q, e)