def mul_cancel

bend-collections-laws-crypto@1.0.0.0 · proofs/math/natural/arith.bend:48

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

48# x c == y c with c > 0 gives x == y   (Mathlib Nat.eq_of_mul_eq_mul_right)
49def mul_cancel(+x: Nat, +y: Nat, +bp: Nat, +e: {Nat.mul(x, 1n+bp) == Nat.mul(y, 1n+bp) : Nat}) -> {x == y : Nat}:
50  match x y:
51    case 0n 0n:
52      {==}
53    case 0n 1n+yp:
54      Empty.absurd({0n == 1n+yp : Nat}, N.zero_succ(Nat.add(bp, Nat.mul(yp, 1n+bp)), e))
55    case 1n+xp 0n:
56      Empty.absurd({1n+xp == 0n : Nat}, N.succ_zero(Nat.add(bp, Nat.mul(xp, 1n+bp)), e))
57    case 1n+ +xp 1n+ +yp:
58      N.succ_cong(xp, yp, mul_cancel(xp, yp, bp, add_cancel(1n+bp, Nat.mul(xp, 1n+bp), Nat.mul(yp, 1n+bp), e)))