def dvd_antisymm

bend-collections-laws-crypto@1.0.0.0 · proofs/math/natural/lcm.bend:39

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

39# x == kx y and y == ky x give x == y   (Mathlib Nat.dvd_antisymm)
40def 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}:
41  match x:
42    case 0n:
43      Equal.sym(Nat, y, 0n, Equal.trans(Nat, y, Nat.mul(ky, 0n), 0n, ey, A.mul_zero(ky)))
44    case 1n+ +xp:
45      +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),
46        A.mul_assoc(kx, ky, 1n+xp),
47        Equal.trans(Nat, Nat.mul(kx, Nat.mul(ky, 1n+xp)), Nat.mul(kx, y), Nat.mul(1n, 1n+xp),
48          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)),
49          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)))))
50      +k1 = mul_eq_one(kx, ky, R.mul_cancel(Nat.mul(kx, ky), 1n, xp, e1))
51      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)))