This is sort of a follow up to a previous question of mine: https://ask.sagemath.org/question/47535/checking-identity-of-two-combinatorial-expressions/
I wanted to prove a certain combinatorial equality. Now, to prove this identity in Sage, I can define the two function $\text{LHS}(n,k)$ and $\text{RHS}(n,k)$ representing the left- and righthand side and make sure that $\text{LHS}(n,k)-\text{RHS}(n,k)=0$ with the following code (actually the code provides a proof of a slightly more general identity, which holds for other values of $n, k$ as well.):
var('n k')
def LHS(n,k):
return n/2*(
(n/2+1-k)/(n/2+1)*((n/2+1)/(k/2)*binomial(n/2-3,k-4)*2**(n/2-k+1)*1/(k/2-1)*binomial(k-4,k/2-2))+
2*(k/2+1)/(n/2+1)*((n/2+1)/(k/2+1)*binomial(n/2-3,k-2)*2**(n/2-k-1)*1/(k/2)*binomial(k-2,k/2-1)))
def RHS(n,k):
return (n/k)*(2**(n/2-k))*binomial(n/2-2,k-2)*binomial(k-2,k/2-1)
(LHS(n,k)-RHS(n,k)).simplify_full()
This outputs
0
which is what I want but I would like to prove this identity with pen-and-paper and this seems to be a bit tricky. I wonder if there is a way to see how exactly simplify_full() were able simplify the expressions?
