def desc_self

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

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/natural.bend as S

84# n.desc(n) == n!   (Mathlib Nat.descFactorial_self)
85def desc_self(+n: Nat) -> {S.desc(n, n) == S.factorial(n) : Nat}:
86  match n:
87    case 0n:
88      {==}
89    case 1n+ +p:
90      Equal.trans(Nat, S.desc(1n+p, 1n+p), Nat.mul(1n+p, S.desc(p, p)), S.factorial(1n+p), desc_succ(p, p), Equal.cong(Nat, Nat, z => Nat.mul(1n+p, z), S.desc(p, p), S.factorial(p), desc_self(p)))