def lt_add_right

bendtorch-core@0.1.0.0 · src/autograd/reduce_replayed_proof.bend:195

import Base
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/storage/api.bend as Api

195def lt_add_right(+a: Nat, +c: Nat, +b: Nat, h: {Nat.is_lt(a, c) == True{} : Bool}) ->
196  {Nat.is_lt(Nat.add(a, b), Nat.add(c, b)) == True{} : Bool}:
197  match a c:
198    case 0n 0n:
199      Empty.absurd({Nat.is_lt(b, b) == True{} : Bool}, Arith.clash(h))
200    case 0n 1n+q:
201      Arith.lt_succ(b, Nat.add(q, b), Api.le_add_left(q, b))
202    case 1n+p 0n:
203      Empty.absurd({Nat.is_lt(1n+Nat.add(p, b), b) == True{} : Bool}, Arith.clash(h))
204    case 1n+p 1n+q:
205      lt_add_right(p, q, b, h)