How to prove the following using invariants? Problem Link: https://cutt.ly/GzRnhPo , slide 38 
Problem : Given numbers 1, 2, 3, ..., 9. 
we place signs + or - to form an expression.
we know that if x is a possible result to such an expression then

*

*x is odd

*-45 <= x <= 45

We want to prove the converse using invariants and the following greedy algorithm: 
Start
from right to left and place the signs greedily:
if the current sum is less than the goal, increase the
sum, otherwise decrease it
Now, my guess for the invariant is the following:

*

*assume that S denote the current remaining sum after some iteration, ex: initially S = x. if we place '-' in front of 9, then S become x-9

*invariant is that (-total <= S <= total), such that total = 0 + 1 + 2 + ... + rightmost number that did not receive a sign yet.

*Initially, the assumed-invariant property holds.   -45 <= S <= 45

*After any iteration, S will be constrained by the suggested invariant.. proving this is my problem!

*This imply that after algorithm is done,   0 <= S <= 0, which mean S = 0, which mean we made an expression with result equal x..

Is my invariant correct ?
How to prove it ? 
Any other ideas to prove same thing using invariants and the provided greedy
 A: Your invariant works until there are only two numbers left for which we need to choose signs. At that point we can easily work out the remaining cases by hand.
Let's call $S_n$ the sum after the $n$-th iteration of your algorithm with $S_0$ being $x$.
Let's prove by induction on $n$ that $|S_n| \le \frac{(9-n) (10-n)}{2}$. This is just the sum that you called total. It's the sum of an arithmetic series.
Base case: if $n = 0$, then $-45 \le x \le 45 \implies |S_0| \le \frac{9 \cdot 10}{2}$.
Now suppose that $|S_n| \le \frac{(9-n) (10-n)}{2}$ for some $0 \le n \le 6$ and let's prove that $|S_{n+1}| \le \frac{(8 - n)(9 - n)}{2}$.
We will split this into two cases:
First if $S_n \le 0$ then $|S_n| = -S_n$. As such, by the induction hypothesis,
$$
0 \le -S_n \le \frac{(9-n) (10-n)}{2} \\
-\frac{(9-n) (10-n)}{2} \le S_n \le 0 \\
-(1 + 2 + 3 + \ldots + (9-n)) \le S_n \le 0
$$
We put a $+$ sign next to $9 - n$: $S_{n+1} = S_n + 9 - n$, as such,
$$
-(1 + 2 + 3 + \ldots (8 - n)) \le S_{n+1} \le 9 - n \le 1 + 2 + \ldots + (8 - n) \\
\implies |S_{n+1}| \le \frac{(8 - n)(9 - n)}{2}
$$
The reasoning is the same for the case $S_n > 0$, we just put a $-$ sign next to $9-n$.
Now we get $|S_7| \le 3$.
$S_7$ is the sum of $8$ numbers $5$ of which are odd (including $x$) so it's odd.
As such, $S_7 = \pm 1$ or $S_7 = \pm 3$.
If $S_7 = 1$, then if we put $-$ next to 2 and $+$ next to 1 we get $S = S_7 - 2 + 1 =0$.
If $S_7 = 3$, then if we put $-$ signs next to both $1$ and $2$ we get $S = S_7 - 2 - 1 = 0$.
For $-1$ and $-3$ just invert the signs.
As such, for every odd integer $x$ in $[-45,45]$ we can get $x$ by placing signs next to the numbers $1,2,\ldots, 9$ and taking the sum.
