Proof step e-bff1938bf7a843de

definition_equality → concludes about Triangular array binomial(2*n-k, k), k=0..n, n >= 0. JSON

Theorem

Ore-algebra identity of two definitions polytool ?

Operation

All-n equality of two definitions

{
  "operation": "definition_equality"
}

Premises

None: this step is a direct theorem check.

Claims

Verification and certificate

• polytool: replayed (the certificate replayed when the step was written)
• Lean: not attempted
• certificate: definition_equality, SHA-256 980e4671d9f4d3de029dc8fa938a8b8d0a22aee5c864ea3e2628b0b2b3d56553, 11,898 bytes (2,956 compressed); download JSON