Fact.desc_succ: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/fact.bend as Fact
Lines 53-60 of bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/fact.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/fact.bend&start_line=53&end_line=60

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/lcm.bend as LC
import bend-collections-laws-crypto@1.0.0.0/spec/math/natural.bend as S

# (1+m).desc(1+j) == (1+m) * m.desc(j)   (Mathlib Nat.succ_descFactorial_succ)
def desc_succ(+m: Nat, +j: Nat) -> {S.desc(1n+m, 1n+j) == Nat.mul(1n+m, S.desc(m, j)) : Nat}:
  match j:
    case 0n:
      {==}
    case 1n+ +i:
      %Equal.sym(Nat, S.desc(1n+m, 1n+i), Nat.mul(1n+m, S.desc(m, i)), desc_succ(m, i)) : {Nat.mul(Nat.sub(m, i), _) == Nat.mul(1n+m, Nat.mul(Nat.sub(m, i), S.desc(m, i))) : Nat}
      LC.swap_cw(Nat.sub(m, i), 1n+m, S.desc(m, i))

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/lcm.bend&name=swap_cw
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/math/natural.bend&name=desc