Lcm.mul_eq_one: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/lcm.bend as Lcm
Lines 26-34 of bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/lcm.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/lcm.bend&start_line=26&end_line=34

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as A

# a b == 1 gives a == 1   (Mathlib Nat.eq_one_of_mul_eq_one_right)
def mul_eq_one(+a: Nat, +b: Nat, +e: {Nat.mul(a, b) == 1n : Nat}) -> {a == 1n : Nat}:
  match a b:
    case 0n b0:
      Empty.absurd({0n == 1n : Nat}, N.zero_succ(0n, e))
    case 1n+ +ap 0n:
      Empty.absurd({1n+ap == 1n : Nat}, N.zero_succ(0n, Equal.trans(Nat, 0n, Nat.mul(1n+ap, 0n), 1n, Equal.sym(Nat, Nat.mul(1n+ap, 0n), 0n, A.mul_zero(1n+ap)), e)))
    case 1n+ +ap 1n+ +bq:
      one_s(ap, bq, N.succ_inj(Nat.add(bq, Nat.mul(ap, 1n+bq)), 0n, e))

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=succ_inj
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=zero_succ
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/lcm.bend&name=one_s