def one_s

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

import Base

19def one_s(+ap: Nat, +bq: Nat, +e: {Nat.add(bq, Nat.mul(ap, 1n+bq)) == 0n : Nat}) -> {1n+ap == 1n : Nat}:
20  match ap:
21    case 0n:
22      {==}
23    case 1n+ +app:
24      Empty.absurd({2n+app == 1n : Nat}, add_succ_zero(bq, Nat.add(bq, Nat.mul(app, 1n+bq)), e))