DotProof.lt_mul_add: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/contracts/dot_proof.bend as DotProof
Lines 52-63 of bendtorch-core@0.1.0.0/src/tensor/contracts/dot_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/contracts/dot_proof.bend&start_line=52&end_line=63

import Base
import bendtorch-core@0.1.0.0/src/shape/index_proofs.bend as Index
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

def lt_mul_add(+a: Nat, +m: Nat, +b: Nat, +n: Nat, a_below: {Nat.is_lt(a, m) == True{} : Bool},
  b_below: {Nat.is_lt(b, n) == True{} : Bool}) -> {Nat.is_lt(Nat.add(Nat.mul(a, n), b), Nat.mul(m, n)) == True{} : Bool}:
  match a m:
    case 0n 0n:
      Empty.absurd({Nat.is_lt(b, 0n) == True{} : Bool}, Arith.clash(a_below))
    case 0n 1n+q:
      Arith.lt_le_trans(b, n, Nat.add(n, Nat.mul(q, n)), b_below, Api.le_add_right(n, Nat.mul(q, n)))
    case 1n+p 0n:
      Empty.absurd({Nat.is_lt(Nat.add(Nat.add(n, Nat.mul(p, n)), b), 0n) == True{} : Bool}, Arith.clash(a_below))
    case 1n+p 1n+q:
      %Index.add_assoc(n, Nat.mul(p, n), b) : {Nat.is_lt(_, Nat.add(n, Nat.mul(q, n))) == True{} : Bool}
      Api.lt_add_left(n, Nat.add(Nat.mul(p, n), b), Nat.mul(q, n), lt_mul_add(p, q, b, n, a_below, b_below))

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/index_proofs.bend&name=add_assoc
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/api.bend&name=le_add_right
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/api.bend&name=lt_add_left
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=clash
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=lt_le_trans