Event: Start with the library "arith".

; Here again is the definition of RAMSEY.

Definition: ramsey (p, q) = if p ≃ 0 then 1

elseif q ≃ 0 then 1

else ramsey (p − 1, q) + ramsey (p, q − 1) endif

Definition: fact (n) = if n ≃ 0 then 1

else n ∗ fact (n − 1) endif

Definition: choose (m, n) = (fact (m) ÷ (fact (n) ∗ fact (m − n)))

Theorem: fact-not-zerop fact (x) ≠ 0

Theorem: ramsey-choose-1 ((fact (p) ∗ fact (q)) ∗ ramsey (p, q)) = fact (p + q)

Theorem: ramsey-choose ramsey (p, q) = choose (p + q, p)

Index

choose, 1

fact, 1 fact-not-zerop, 1

ramsey, 1 ramsey-choose, 1 ramsey-choose-1, 1