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

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as A
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend as R

# x == kx y and y == ky x give x == y   (Mathlib Nat.dvd_antisymm)
def dvd_antisymm(+x: Nat, +y: Nat, +kx: Nat, +ky: Nat, +ex: {x == Nat.mul(kx, y) : Nat}, +ey: {y == Nat.mul(ky, x) : Nat}) -> {x == y : Nat}:
  match x:
    case 0n:
      Equal.sym(Nat, y, 0n, Equal.trans(Nat, y, Nat.mul(ky, 0n), 0n, ey, A.mul_zero(ky)))
    case 1n+ +xp:
      +e1 = Equal.trans(Nat, Nat.mul(Nat.mul(kx, ky), 1n+xp), Nat.mul(kx, Nat.mul(ky, 1n+xp)), Nat.mul(1n, 1n+xp),
        A.mul_assoc(kx, ky, 1n+xp),
        Equal.trans(Nat, Nat.mul(kx, Nat.mul(ky, 1n+xp)), Nat.mul(kx, y), Nat.mul(1n, 1n+xp),
          Equal.cong(Nat, Nat, z => Nat.mul(kx, z), Nat.mul(ky, 1n+xp), y, Equal.sym(Nat, y, Nat.mul(ky, 1n+xp), ey)),
          Equal.trans(Nat, Nat.mul(kx, y), 1n+xp, Nat.mul(1n, 1n+xp), Equal.sym(Nat, 1n+xp, Nat.mul(kx, y), ex), Equal.sym(Nat, Nat.mul(1n, 1n+xp), 1n+xp, one_mul(1n+xp)))))
      +k1 = mul_eq_one(kx, ky, R.mul_cancel(Nat.mul(kx, ky), 1n, xp, e1))
      Equal.trans(Nat, 1n+xp, Nat.mul(kx, y), y, ex, Equal.trans(Nat, Nat.mul(kx, y), Nat.mul(1n, y), y, Equal.cong(Nat, Nat, z => Nat.mul(z, y), kx, 1n, k1), one_mul(y)))

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  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.mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/arith.bend&name=mul_cancel
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/lcm.bend&name=mul_eq_one
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/natural/lcm.bend&name=one_mul