def comb_min

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

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/spec/math/natural.bend as S

261def comb_min(+n: Nat, +k: Nat, +hk: {Nat.is_le(k, n) == True{} : Bool}, +b: Bool, +hb: {Nat.is_lt(k, Nat.sub(n, k)) == b : Bool}) -> {S.choose(n, Nat.min(k, Nat.sub(n, k))) == S.choose(n, k) : Nat}:
262  match b:
263    case True{}:
264      Equal.cong(Nat, Nat, z => S.choose(n, z), Nat.min(k, Nat.sub(n, k)), k, N.min_left(k, Nat.sub(n, k), hb))
265    case False{}:
266      Equal.trans(Nat, S.choose(n, Nat.min(k, Nat.sub(n, k))), S.choose(n, Nat.sub(n, k)), S.choose(n, k), Equal.cong(Nat, Nat, z => S.choose(n, z), Nat.min(k, Nat.sub(n, k)), Nat.sub(n, k), N.min_right(k, Nat.sub(n, k), hb)), choose_symm(n, k, hk))