def lt_add_right

bendtorch-core@0.1.0.0 · src/tensor/contracts/build_facts.bend:83

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

83def lt_add_right(+a: Nat, +c: Nat, +b: Nat, h: {Nat.is_lt(a, c) == True{} : Bool}) ->
84  {Nat.is_lt(Nat.add(a, b), Nat.add(c, b)) == True{} : Bool}:
85  match a c:
86    case 0n 0n:
87      Empty.absurd({Nat.is_lt(b, b) == True{} : Bool}, Arith.clash(h))
88    case 0n 1n+q:
89      Arith.lt_succ(b, Nat.add(q, b), Api.le_add_left(q, b))
90    case 1n+p 0n:
91      Empty.absurd({Nat.is_lt(1n+Nat.add(p, b), b) == True{} : Bool}, Arith.clash(h))
92    case 1n+p 1n+q:
93      lt_add_right(p, q, b, h)