Some step need to be improved in polynomial transformation

[kidherofun]

Question from minif2f (mathd_numbertheory_430):

If $A$, $B$, and $C$ represent three distinct digits from 1 to 9 and they satisfy the following equations, what is the value of the sum $A+B+C$? (In the equation below, $AA$ represents a two-digit number both of whose digits are $A$.) $$A+B=C$$, $$AA-B=2\times C$$, $$C\times B=AA+A$$ Show that it is 8

Solution in Litex:

claim:
    forall a, b, c N_pos:
        a >= 1
        a <= 9
        b >= 1
        b <= 9
        c >= 1
        c <= 9
        a != 0
        b != 0
        c != 0
        a != b
        a != c
        b != c
        a + b = c
        10 * a + a - b = 2 * c
        c * b = 10 * a + a + a
        =>:
            a + b + c = 8
    prove:
        c = a + b
        10 * a + a - b = 2 * (a + b)
        10 * a + a - b = 2 * a + 2 * b
        11 * a - b = 2 * a + 2 * b
        11 * a - b - 2 * a = 2 * b
        11 * a - 2 * a = 2 * b + b
        9 * a = 2 * b + b
        9 * a = 3 * b
        9 * a / 3 = b
        3 * a = b
        c * b = 10 * a + a + a
        c * b = 12 * a
        (a + b) * b = 12 * a
        (a + 3 * a) * (3 * a) = 12 * a
        4 * a * 3 * a = 12 * a
        12 * a * a = 12 * a
        12 * a * a - 12 * a = 0
        12 * (a * a - a) = 0
        a * a - a = 0 / 12 = 0
        a * (a - 1) = 0
        a - 1 = 0 / a = 0
        a - 1 + 1 = 0 + 1 = 1
        a = 1
        b = 3 * a = 3 * 1 = 3
        c = a + b = 1 + 3 = 4
        a + b + c = 1 + 3 + 4 = 8

It's too long to solve it. There are some advice for based on this case:

1. For steps: 10 * a + a - b = 2 * a + 2 * b -> 11 * a - b = 2 * a + 2 * b -> 11 * a - b - 2 * a = 2 * b -> 11 * a - 2 * a = 2 * b + b, it's better to be: 10 * a + a - b = 2 * a + 2 * b -> 11 * a - 2 * a = 2 * b + b
2. For steps: 9 * a = 3 * b -> 9 * a / 3 = b -> 3 * a = b, it's better to be: 9 * a = 3 * b -> 3 * a = b
3. For steps: a - 1 = 0 -> a - 1 + 1 = 0 + 1 = 1 -> a = 1, it's better to be a - 1 = 0 -> a = 1
4. For steps: 12 * (a * a - a) = 0 -> a * a - a = 0 / 12 = 0, it's better to remove = 0/ 12 part
5. For steps: a * (a - 1) = 0 -> a - 1 = 0 / a = 0, it's better to remove = 0/a part if a != 0 is proved
6. Support a >= 1 -> a != 0 by default
7. Support 1 <= a <= 9 instead of a >= 1, a <= 9

[malloc-realloc]

本质上是 消去律和传递性 写起来有点烦