def mul_eq_one

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

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

26# a b == 1 gives a == 1   (Mathlib Nat.eq_one_of_mul_eq_one_right)
27def mul_eq_one(+a: Nat, +b: Nat, +e: {Nat.mul(a, b) == 1n : Nat}) -> {a == 1n : Nat}:
28  match a b:
29    case 0n b0:
30      Empty.absurd({0n == 1n : Nat}, N.zero_succ(0n, e))
31    case 1n+ +ap 0n:
32      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)))
33    case 1n+ +ap 1n+ +bq:
34      one_s(ap, bq, N.succ_inj(Nat.add(bq, Nat.mul(ap, 1n+bq)), 0n, e))