Nat.internal_lt_mul_two_add: def of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/nat.bend as Nat
Lines 3360-3365 of bend-mathlib@0.8.1.0/nat.bend: https://jend.leeeet.dev/read.txt?path=bend-mathlib@0.8.1.0/nat.bend&start_line=3360&end_line=3365

import Base

def internal_lt_mul_two_add(a: Nat, x: Nat, hx: lt(0n, x)) -> lt(x, Nat.mul(2n+a, x)):
  match x:
    case 0n:
      Empty.absurd(lt(0n, Nat.mul(2n+a, 0n)), internal_false_ne_true(hx))
    case 1n++y:
      lt_add_of_pos_right(y, Nat.add(y, Nat.mul(a, 1n+y)))

Uses (7):
  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.mul
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=internal_false_ne_true
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=lt
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/nat.bend&name=lt_add_of_pos_right