Fact.choose_symm: 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 236-246 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=236&end_line=246

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as A
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

# C(n, n - k) == C(n, k)   (Mathlib Nat.choose_symm)
def choose_symm(+n: Nat, +k: Nat, +h: {Nat.is_le(k, n) == True{} : Bool}) -> {S.choose(n, Nat.sub(n, k)) == S.choose(n, k) : Nat}:
  +kk = Nat.sub(n, k)
  +fk = S.factorial(k)
  +fkk = S.factorial(kk)
  +e1 = choose_mul_facts(n, kk, sub_le_self(n, k))
  +e1b = Equal.trans(Nat, Nat.mul(S.choose(n, kk), Nat.mul(fkk, fk)), Nat.mul(S.choose(n, kk), Nat.mul(fkk, S.factorial(Nat.sub(n, kk)))), S.factorial(n),
    Equal.cong(Nat, Nat, z => Nat.mul(S.choose(n, kk), Nat.mul(fkk, S.factorial(z))), k, Nat.sub(n, kk), Equal.sym(Nat, Nat.sub(n, kk), k, sub_sub_self(n, k, h))), e1)
  +e2 = Equal.trans(Nat, Nat.mul(S.choose(n, k), Nat.mul(fkk, fk)), Nat.mul(S.choose(n, k), Nat.mul(fk, fkk)), S.factorial(n),
    Equal.cong(Nat, Nat, z => Nat.mul(S.choose(n, k), z), Nat.mul(fkk, fk), Nat.mul(fk, fkk), A.mul_comm(fkk, fk)), choose_mul_facts(n, k, h))
  LC.cancel_pos(S.choose(n, kk), S.choose(n, k), Nat.mul(fkk, fk), pos_pos(fkk, fk, factorial_pos(kk), factorial_pos(k)), Equal.trans(Nat, Nat.mul(S.choose(n, kk), Nat.mul(fkk, fk)), S.factorial(n), Nat.mul(S.choose(n, k), Nat.mul(fkk, fk)), e1b, Equal.sym(Nat, Nat.mul(S.choose(n, k), Nat.mul(fkk, fk)), S.factorial(n), e2)))

Uses (17):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  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/lib/lemmas/proofs/nat_algebra.bend&name=mul_comm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/fact.bend&name=choose_mul_facts
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/fact.bend&name=factorial_pos
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/fact.bend&name=pos_pos
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/fact.bend&name=sub_le_self
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/fact.bend&name=sub_sub_self
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/lcm.bend&name=cancel_pos
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/math/natural.bend&name=choose
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/math/natural.bend&name=factorial