def desc_succ

bend-collections-laws-crypto@1.0.0.0 · proofs/math/natural/fact.bend:53

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

53# (1+m).desc(1+j) == (1+m) * m.desc(j)   (Mathlib Nat.succ_descFactorial_succ)
54def desc_succ(+m: Nat, +j: Nat) -> {S.desc(1n+m, 1n+j) == Nat.mul(1n+m, S.desc(m, j)) : Nat}:
55  match j:
56    case 0n:
57      {==}
58    case 1n+ +i:
59      %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}
60      LC.swap_cw(Nat.sub(m, i), 1n+m, S.desc(m, i))