Proof step e-f417b7c94fe88fc7

definition_equality → concludes about Triangle T(n, k) is coefficient of z^n*w^k in 1/(1 - 2*z - 2*w - 2*z*w) read by rows in order 00, 10, 01, 20, 11, 02, ... 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 6364903bf40209aa10c91e191d5da32ad023b3bf48cee95931c7df5b68ff7b93, 20,478 bytes (4,751 compressed); download JSON